`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitZeroLeIffNonnegFlagChoiceFree`

IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Grow/SignedOrbitZeroLeIffNonnegFlagChoiceFree.lean · 24 lines · 1 declarations

show as: view math explainer →

open module explainer GitHub source

Explainer status: pending

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit
   5import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic
   6import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree
   7
   8namespace IndisputableMonolith.PRCGrow.SignedOrbitZeroLeIffNonnegFlagChoiceFree
   9
  10open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  11open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  12
  13theorem zero_le_iff_nonnegFlag_cf (z : SignedOrbit) :
  14    SignedOrbit.le SignedOrbit.zero z ↔ z.nonnegFlag = true := by
  15  rw [le_iff_nonnegFlag_sub_cf]
  16  unfold SignedOrbit.nonnegFlag
  17  rw [leq_eq_true_iff_cf, leq_eq_true_iff_cf]
  18  have hp : (SignedOrbit.sub z SignedOrbit.zero).pos = z.pos + DistinctionNat.zero := rfl
  19  have hn : (SignedOrbit.sub z SignedOrbit.zero).neg = z.neg + DistinctionNat.zero := rfl
  20  rw [hp, hn, DistinctionNat.toNat_add, DistinctionNat.toNat_add,
  21      DistinctionNat.toNat_zero, Nat.add_zero, Nat.add_zero]
  22
  23end IndisputableMonolith.PRCGrow.SignedOrbitZeroLeIffNonnegFlagChoiceFree
  24

source mirrored from github.com/jonwashburn/shape-of-logic