> module nat_ord where;

> import nat_times;

Ordering Relations

Weak inequality

> [le [m, n : Nat] = ex nat [p : Nat] eq nat (plus p m) n];
> [Le [m, n : Nat] = Ex Nat [p : Nat] Eq nat (plus p m) n];

> Claim LeI : (m, n, p : Nat) Eq nat (plus p m) n -> Le m n;
> Intros m n;
> Refine ExI Nat [p : Nat] Eq nat (plus p m) n;
> ReturnAll;
> LeI;

> Claim LeI' : (m, n, p : Nat) Eq nat (plus m p) n -> Le m n;
> Intros m n p mp_is_n;
> Refine LeI;
> Refine trans;
> Refine mp_is_n;
> Refine plus_comm p;
> ReturnAll;
> LeI';

> Claim LeE : (m,n : Nat) (P : Prop) ((p : Nat) Eq nat (plus p m) n -> P) -> Le m n -> P;
> Intros m n;
> Refine ExE Nat [p : Nat] Eq nat (plus p m) n;
> ReturnAll;
> LeE;

> Claim zero_Le : (n : Nat) Le zero n;
> Intros n;
> Refine LeI ? ? n;
> Refine EqI;
> ReturnAll;
> zero_Le;

> Claim succ_Le_succ : (m, n : Nat) Le m n -> Le (succ m) (succ n);
> Intros m n;
> Refine LeE m n;
> Intros p pm_is_n;
> Refine LeI ? ? p;
> Refine wd nat nat succ;
> Refine pm_is_n;
> ReturnAll;
> succ_Le_succ;

> Claim succ_Le_succ_cancel : (m, n : Nat) Le (succ m) (succ n) -> Le m n;
> Intros m n;
> Refine LeE;
> Intros p pSm_is_Sn;
> Refine LeI;
> 2 Refine p;
> Refine Peano3;
> Refine pSm_is_Sn;
> ReturnAll;
> succ_Le_succ_cancel;

> Claim Le_ref : (n : Nat) Le n n;
> Intros n;
> Refine LeI;
> Refine zero_plus;
> ReturnAll;
> Le_ref;

> Claim Le_trans : (m, n, p : Nat) Le m n -> Le n p -> Le m p;
> Intros m n p m_le_n n_le_p;
> Refine LeE m n;
> Refine m_le_n;
> Intros k H;
> Refine LeE n p;
> Refine n_le_p;
> Intros l K;
> Refine LeI;
> Refine trans;
> Refine K;
> Refine trans;
> Refine wd nat nat (plus l) ? ? H;
> Refine plus_assocr;
> ReturnAll;
> Le_trans;

> Claim Le_antisym : (m, n : Nat) Le m n -> Le n m -> Eq nat m n;
> Intros m n m_le_n n_le_m;
> Refine LeE m n;
> Refine m_le_n;
> Intros k H;
> Refine LeE n m;
> Refine n_le_m;
> Intros l K;
> Claim step1 : Eq nat (plus zero n) n;
> Refine zero_plus;
> Claim step2 : Eq nat (plus zero n) (plus k (plus l n));
> Refine trans;
> 2 Refine step1;
> Refine sym;
> Refine trans;
> Refine H;
> Refine wd nat nat (plus k);
> Refine K;
> Claim step3 : Eq nat (plus zero n) (plus (plus k l) n);
> Refine trans;
> 2 Refine step2;
> Refine plus_assocl;
> Claim step4 : Eq nat zero (plus k l);
> Refine plus_cancelr;
> Refine step3;
> Claim step5 : Eq nat l zero;
> Refine m_plus_n_is_zeror;
> Refine sym;
> Refine step4;
> Refine trans;
> 2 Refine sym;
> 2 Refine K;
> Refine trans;
> 2 Refine wd nat nat ([x : Nat] plus x n) ? ? step5;
> Refine zero_plus;
> ReturnAll;
> Le_antisym;

> Claim Thm4_17 : (m, n : Nat) Or (Le m n) (Le (succ n) m);
> Intros m n;
> Refine Ind_Nat [m : Nat] or (le m n) (le (succ n) m);
> 2 Refine OrI1;
> 2 Refine zero_Le;
> Intros m';
> Refine OrE;
Case One: m' <= n
> 2 Refine LeE;
> 2 Intros k H;
> Refine OrE;
> Refine zero_or_succ k;
If k = 0:
> 2 Intros k_is_zero;
> Claim n_is_m' : Eq nat n m';
> Refine trans;
> Refine zero_plus;
> Refine trans;
> 2 Refine sym;
> 2 Refine H;
> Refine wd nat nat ([x : Nat] plus x m') ? ? k_is_zero;
> Claim case11 : Eq nat (plus zero (succ n)) (succ m');
> Refine trans;
> 2 Refine zero_plus (succ n);
> Refine wd nat nat succ;
> Refine n_is_m';
> Refine OrI2;
> Refine LeI;
> Refine case11;
> ReturnAll;
If k = succ l:
> Refine ExE Nat;
> Intros l k_is_Sl;
> Claim Case12b : Eq nat n (plus (succ l) m');
> Refine trans;
> 2 Refine sym;
> 2 Refine H;
> Refine wd nat nat ([x : Nat] plus x m') ? ? k_is_Sl;
> Claim Case12c : Eq nat n (plus l (succ m'));
> Refine trans;
> 2 Refine Case12b;
> Refine sym;
> Refine succ_plus;
> Refine OrI1;
> Refine LeI;
> Refine sym;
> Refine Case12c;
> ReturnAll;
Case Two : succ n <= m
> Refine LeE (succ n) m';
> Intros k H;
> Claim Case2 : Eq nat (plus (succ k) (succ n)) (succ m');
> Refine trans;
> Refine wd nat nat succ ? ? H;
> Refine sym;
> Refine succ_plus k (succ n);
> Refine OrI2;
> Refine LeI;
> Refine Case2;
> ReturnAll;
> Thm4_17;

> Claim Le_total : (m, n : Nat) Or (Le m n) (Le n m);
> Intros m n;
> Refine OrE;
> Refine Thm4_17 m n;
> 2 Refine OrI1;
> Refine LeE;
> Intros p pSn_is_m;
> Refine OrI2;
> Refine LeI;
> Refine trans;
> Refine pSn_is_m;
> Refine sym;
> Refine succ_plus;
> ReturnAll;
> Le_total;

> Claim Eq_Le : (m, n : Nat) Eq nat m n -> Le m n;
> Intros m n m_is_n;
> Refine LeI;
> Refine trans;
> Refine m_is_n;
> Refine zero_plus;
> ReturnAll;
> Eq_Le;

> Claim Le_plusr : (m, n, p : Nat) Le m n -> Le (plus m p) (plus n p);
> Intros m n p;
> Refine LeE;
> Intros q q_plus_m_is_n;
> Refine LeI;
> Refine trans;
> 2 Refine plus_assocl q m p;
> Refine wd nat nat [z : Nat] plus z p;
> Refine q_plus_m_is_n;
> ReturnAll;
> Le_plusr;

> Claim Le_plusl : (m, n, p : Nat) Le n p -> Le (plus m n) (plus m p);
> Intros m n p n_le_p;
> Refine EqE2 nat nat Le;
> Refine Le_plusr n p m;
> Refine n_le_p;
> Refine plus_comm;
> Refine plus_comm;
> ReturnAll;
> Le_plusl;

> Claim Le_plus_cancelr : (m, n, p : Nat) Le (plus m p) (plus n p) -> Le m n;
> Intros m n p;
> Refine LeE;
> Intros k kmp_is_np;
> Refine LeI m n k;
> Refine plus_cancelr ? ? p;
> Refine trans;
> Refine kmp_is_np;
> Refine plus_assocr;
> ReturnAll;
> Le_plus_cancelr;

> Claim Le_plus_cancell : (m, n, p : Nat) Le (plus m n) (plus m p) -> Le n p;
> Intros m n p mn_le_mp;
> Refine Le_plus_cancelr n p m;
> Refine EqE2 nat nat Le (plus m n) (plus n m) (plus m p) (plus p m);
> Refine mn_le_mp;
> Refine plus_comm;
> Refine plus_comm;
> ReturnAll;
> Le_plus_cancell;

> Claim Le_timesr : (m, n, p : Nat) Le m n -> Le (times m p) (times n p);
> Intros m n p;
> Refine LeE;
> Intros k km_is_n;
> Refine LeI;
> 2 Refine (times k p);
> Refine trans nat ? (times (plus k m) p);
> 2 Refine times_plus_distr';
> Refine wd nat nat [z : Nat] times z p;
> Refine km_is_n;
> ReturnAll;
> Le_timesr;

> Claim Le_timesl : (m, n, p : Nat) Le m n -> Le (times p m) (times p n);
> Intros m n p m_le_n;
> Refine EqE2 nat nat Le;
> 2 Refine times_comm;
> 2 Refine times_comm;
> Refine Le_timesr;
> Refine m_le_n;
> ReturnAll;
> Le_timesl;

Strict inequality

> [lt [m, n : Nat] = ex nat [p : Nat] eq nat (plus (succ p) m) n];
> [Lt [m, n : Nat] = Ex Nat [p : Nat] Eq nat (plus (succ p) m) n];

> Claim LtI : (m, n, p : Nat) Eq nat (plus (succ p) m) n -> Lt m n;
> Intros m n;
> Refine ExI Nat [p : Nat] Eq nat (plus (succ p) m) n;
> ReturnAll;
> LtI;

> Claim LtE : (m, n : Nat) (Q : Prop) ((p : Nat) Eq nat (plus (succ p) m) n -> Q) -> Lt m n -> Q;
> Intros m n;
> Refine ExE Nat [p : Nat] Eq nat (plus (succ p) m) n;
> ReturnAll;
> LtE;

> Claim not_Lt_zero : (n : Nat) Lt n zero -> False;
> Intros n;
> Refine LtE;
> Intros k Skn_is_0;
> Refine Peano4';
> Refine m_plus_n_is_zerol;
> Refine Skn_is_0;
> ReturnAll;
> not_Lt_zero;

> Claim Lt_succ : (n : Nat) Lt n (succ n);
> Intros n;
> Refine LtI;
> Refine trans;
> Refine zero_plus;
> Refine sym;
> Refine succ_plus;
> ReturnAll;
> Lt_succ;

> Claim succ_Lt_succ : (m, n : Nat) Lt m n -> Lt (succ m) (succ n);
> Intros m n;
> Refine LtE;
> Intros k Skm_is_n;
> Refine LtI;
> Refine wd nat nat succ;
> Refine Skm_is_n;
> ReturnAll;
> succ_Lt_succ;

> Claim succ_Lt_succ_cancel : (m, n : Nat) Lt (succ m) (succ n) -> Lt m n;
> Intros m n;
> Refine LtE;
> Intros k SkSm_is_Sn;
> Refine LtI;
> Refine Peano3;
> Refine SkSm_is_Sn;
> ReturnAll;
> succ_Lt_succ_cancel;

> Claim Lt_irref : (n : Nat) Lt n n -> False;
> Intros n;
> Refine LtE;
> Intros k Skn_is_n;
> Claim zeron_is_Skn : Eq nat (plus zero n) (plus (succ k) n);
> Refine trans;
> Refine sym;
> Refine Skn_is_n;
> Refine zero_plus;
> Claim zero_is_Sk : Eq nat zero (succ k);
> Refine plus_cancelr;
> Refine zeron_is_Skn;
> Refine Peano4';
> Refine sym;
> Refine zero_is_Sk;
> ReturnAll;
> Lt_irref;

> Claim Lt_trans : (m, n, p : Nat) Lt m n -> Lt n p -> Lt m p;
> Intros m n p m_lt_n;
> Refine LtE;
> Intros l Sln_is_p;
> Refine LtE m n;
> Refine m_lt_n;
> Intros k Skm_is_n;
> Claim p_is_SlSkm : Eq nat p (plus (succ l) (plus (succ k) m));
> Refine trans;
> Refine wd nat nat (plus (succ l)) n;
> Refine sym;
> Refine Skm_is_n;
> Refine sym;
> Refine Sln_is_p;
> Claim p_is_SlSk_m : Eq nat p (plus (plus (succ l) (succ k)) m);
> Refine trans;
> Refine plus_assocl;
> Refine p_is_SlSkm;
> Refine LtI;
> Refine sym;
> Refine p_is_SlSk_m;
> ReturnAll;
> Lt_trans;

> Claim Lt_asym : (m, n : Nat) Lt m n -> Lt n m -> False;
> Intros m n m_lt_n n_lt_m;
> Refine Lt_irref;
> Refine Lt_trans;
> Refine n_lt_m;
> Refine m_lt_n;
> ReturnAll;
> Lt_asym;

> Claim Lt_asym' : (m, n : Nat) (P : Prop) Lt m n -> Lt n m -> P;
> Intros m n P m_lt_n n_lt_m;
> Refine FalseE;
> Refine Lt_asym;
> Refine n_lt_m;
> Refine m_lt_n;
> ReturnAll;
> Lt_asym';

> Claim trichotomy : (m, n : Nat) Or (Or (Lt m n) (Eq nat m n)) (Lt n m);
> Intros m;
> Refine Ind_Nat [n : Nat] or (or (lt m n) (eq nat m n)) (lt n m);
Base Case
> 2 Refine OrE;
> 2 Refine zero_or_succ m;
> 3 Intros m_is_0;
> Refine OrI1;
> Refine OrI2;
> Refine m_is_0;
> ReturnAll;
> 2 Refine ExE;
> 2 Intros k m_is_Sk;
> Refine OrI2;
> Refine LtI;
> Refine sym;
> Refine m_is_Sk;
> ReturnAll;
Induction Step
> Intros n;
> Refine OrE;
Case One - m < n or m = n
> 2 Intros CaseOne;
> Refine OrI1;
> Refine OrI1;
> Refine OrE;
> Refine CaseOne;
Case m = n
> Intros m_is_n;
> Refine LtI ? ? zero;
> Refine trans;
> Refine wd nat nat succ m;
> Refine m_is_n;
> Refine trans;
> 3 Refine succ (plus zero m);
> Refine wd nat nat succ;
> Refine zero_plus;
> Refine sym;
> Refine succ_plus;
> ReturnAll;
Case m < n
> Refine LtE;
> Intros k Sk_m_is_n;
> Refine LtI;
> 2 Refine (succ k);
> Refine trans;
> 3 Refine succ (plus (succ k) m);
> Refine wd nat nat succ;
> Refine Sk_m_is_n;
> Refine sym;
> Refine succ_plus;
> ReturnAll;
Case 2 - n < m
> Refine LtE;
> Intros k Sk_n_is_m;
> Refine OrE;
> Refine zero_or_succ k;
Case k = 0
> 2 Intros k_is_zero;
> Refine OrI1;
> Refine OrI2;
> Refine trans;
> 2 Refine sym;
> 2 Refine Sk_n_is_m;
> Refine trans;
> 3 Refine plus (succ zero) n;
> Refine trans;
> Refine wd nat nat succ (plus zero n);
> Refine zero_plus;
> Refine sym;
> Refine succ_plus;
> Refine wd nat nat [z : Nat] plus (succ z) n;
> Refine k_is_zero;
> ReturnAll;
Case k = S[l]
> Refine ExE;
> Intros l k_is_Sl;
> Refine OrI2;
> Refine LtI;
> 2 Refine l;
> Refine trans;
> Refine Sk_n_is_m;
> Refine trans;
> Refine succ_plus;
> Refine wd nat nat [z : Nat] plus z (succ n);
> Refine sym;
> Refine k_is_Sl;
> ReturnAll;
> trichotomy;

> Claim trichotomy' : (m, n : Nat) (P : Prop) (Lt m n -> P) -> (Eq nat m n -> P) -> (Lt n m -> P) -> P;
> Intros m n P H1 H2 H3;
> Refine OrE;
> Refine trichotomy m n;
> Refine H3;
> Refine OrE;
> Refine H2;
> Refine H1;
> ReturnAll;
> trichotomy';

> Claim Lt_neq : (m, n : Nat) Lt m n -> Neq nat m n;
> Intros m n;
> Refine LtE;
> Intros p Sp_plus_m_is_n;
> Refine NotI;
> Intros m_is_n;
> Refine Peano4' p;
> Refine plus_cancelr ? ? m;
> Refine trans nat ? n;
> 2 Refine Sp_plus_m_is_n;
> Refine sym;
> Refine trans;
> Refine m_is_n;
> Refine zero_plus;
> ReturnAll;
> Lt_neq;

> Claim Lt_neq' : (m, n : Nat) (P : Prop) Lt m n -> Eq nat m n -> P;
> Intros m n P m_lt_n;
> Refine NotE';
> Refine Lt_neq;
> Refine m_lt_n;
> ReturnAll;
> Lt_neq';

> Claim Lt_plusr : (m, n, p : Nat) Lt m n -> Lt (plus m p) (plus n p);
> Intros m n p;
> Refine ImpE;
> Refine Ind_Nat [p : Nat] imp (lt m n) (lt (plus m p) (plus n p));
> 2 Refine ImpI;
> 2 Refine [H : ?] H;
> Intros p ih;
> Refine ImpI;
> Intros m_lt_n;
> Refine succ_Lt_succ;
> Refine ImpE;
> 2 Refine ih;
> Refine m_lt_n;
> ReturnAll;
> Lt_plusr;

> Claim Lt_plusl : (m, n, p : Nat) Lt n p -> Lt (plus m n) (plus m p);
> Intros m n p n_lt_p;
> Refine EqE2 nat nat Lt (plus n m) ? (plus p m);
> 3 Refine plus_comm;
> 2 Refine plus_comm;
> Refine Lt_plusr;
> Refine n_lt_p;
> ReturnAll;
> Lt_plusl;

> Claim Lt_plus_cancelr : (m, n, p : Nat) Lt (plus m p) (plus n p) -> Lt m n;
> Intros m n p;
> Refine LtE;
> Intros k Skmp_is_np;
> Refine LtI;
> 2 Refine k;
> Refine plus_cancelr;
> 2 Refine p;
> Refine trans nat ? (plus (succ k) (plus m p));
> Refine Skmp_is_np;
> Refine plus_assocr;
> ReturnAll;
> Lt_plus_cancelr;

> Claim Lt_plus_cancell : (m, n, p : Nat) Lt (plus m n) (plus m p) -> Lt n p;
> Intros m n p mn_lt_mp;
> Refine Lt_plus_cancelr;
> Refine EqE2 nat nat Lt (plus m n) ? (plus m p);
> Refine mn_lt_mp;
> Refine plus_comm;
> Refine plus_comm;
> ReturnAll;
> Lt_plus_cancell;

> Claim Lt_timesr : (m, n, p : Nat) Lt m n -> Neq nat p zero -> Lt (times m p) (times n p);
> Intros m n p m_lt_n;
> Refine not_zero_succ;
> Intros q p_is_Sq;
> Refine LtE m n;
> Refine m_lt_n;
> Intros k Sk_plus_m_is_n;
> Refine LtI;
> Refine trans;
> Refine wd nat nat ([x : Nat] times x p) ? ? Sk_plus_m_is_n;
> Refine transr;
> Refine times_plus_distr;
> Refine wd nat nat [x : Nat] plus x (times m p);
> 2 Refine (plus (times (succ k) q) k);
> Refine wd nat nat (times (succ k)) (succ q) p;
> Refine sym;
> Refine p_is_Sq;
> ReturnAll;
> Lt_timesr;

> Claim Lt_timesl : (m, n, p : Nat) Lt n p -> Neq nat m zero -> Lt (times m n) (times m p);
> Intros m n p n_lt_p zero_not_m;
> Refine EqE2 nat nat Lt (times n m) ? (times p m);
> Refine Lt_timesr;
> Refine zero_not_m;
> Refine n_lt_p;
> Refine times_comm;
> Refine times_comm;
> ReturnAll;
> Lt_timesl;

> Claim Lt_times_cancelr : (m, n, p : Nat) Lt (times m p) (times n p) -> Lt m n;
> Intros m n p mp_lt_np;
> Refine trichotomy' m n;
> 3 Intros m_lt_n;
> Refine m_lt_n;
> ReturnAll;
> 2 Intros m_is_n;
> Refine Lt_neq';
> 2 Refine mp_lt_np;
> Refine wd nat nat [t : Nat] times t p;
> Refine m_is_n;
> ReturnAll;
> Intros n_lt_m;
> Refine Lt_asym' (times m p) (times n p);
> 2 Refine mp_lt_np;
> Refine Lt_timesr;
> 2 Refine n_lt_m;
> Refine NotI;
> Intros p_is_zero;
> Refine Lt_irref zero;
> Refine EqE nat (Lt zero) (times n p) zero;
> 2 Refine EqE nat ([t : Nat] Lt t (times n p)) (times m p);
> 3 Refine mp_lt_np;
> 2 Refine wd nat nat (times m) p zero;
> 2 Refine p_is_zero;
> Refine wd nat nat (times n) p zero;
> Refine p_is_zero;
> ReturnAll;
> Lt_times_cancelr;

> Claim Lt_times_cancell : (m, n, p : Nat) Lt (times m n) (times m p) -> Lt n p;
> Intros m n p mn_lt_mp;
> Refine Lt_times_cancelr n p m;
> Refine EqE2 nat nat Lt;
> 2 Refine times_comm;
> 2 Refine times_comm;
> Refine mn_lt_mp;
> ReturnAll;
> Lt_times_cancell;

> Claim times_cancelr : (m, n, p : Nat) Eq nat (times m p) (times n p) -> Neq nat p zero -> Eq nat m n;
> Intros m n p mp_is_np p_not_zero;
> Refine trichotomy' m n;
> Intros n_lt_m;
> Refine NotE';
> Refine sym nat (times m p) (times n p);
> Refine mp_is_np;
> Refine Lt_neq;
> Refine Lt_timesr;
> Refine p_not_zero;
> Refine n_lt_m;
> ReturnAll;
> Intros m_is_n;
> Refine m_is_n;
> ReturnAll;
> Intros m_lt_n;
> Refine NotE';
> Refine mp_is_np;
> Refine Lt_neq;
> Refine Lt_timesr;
> Refine p_not_zero;
> Refine m_lt_n;
> ReturnAll;
> times_cancelr;

> Claim times_cancell : (m, n, p : Nat) Eq nat (times m n) (times m p) -> Neq nat m zero -> Eq nat n p;
> Intros m n p mn_is_mp;
> Refine times_cancelr;
> Refine trans nat ? (times m n);
> 2 Refine times_comm;
> Refine trans nat ? (times m p);
> 2 Refine mn_is_mp;
> Refine times_comm;
> ReturnAll;
> times_cancell;

Relations between the two

> Claim Le_Lt_or_eq : (m, n : Nat) Le m n -> Or (Lt m n) (Eq nat m n);
> Intros m n;
> Refine LeE;
> Intros p p_plus_m_is_n;
> Refine OrE;
> Refine zero_or_succ p;
Case p = 0
> 2 Intros p_is_zero;
> Refine OrI2;
> Refine EqE nat [z : Nat] Eq nat z n;
> 2 Refine p_plus_m_is_n;
> Refine trans nat ? (plus zero m);
> Refine zero_plus;
> Refine wd nat nat ([z : Nat] plus z m) p zero;
> Refine p_is_zero;
> ReturnAll;
Case p = succ q
> Refine ExE;
> Intros q p_is_Sq;
> Refine OrI1;
> Refine LtI;
> Refine EqE nat [z : Nat] Eq nat (plus z m) n;
> Refine p_is_Sq;
> Refine p_plus_m_is_n;
> ReturnAll;
> Le_Lt_or_eq;

> Claim Lt_Le : (m, n : Nat) Lt m n -> Le m n;
> Intros m n;
> Refine LtE;
> Intros p;
> Refine LeI;
> ReturnAll;
> Lt_Le;

> Claim Le_Neq_Lt : (m, n : Nat) Le m n -> Neq nat m n -> Lt m n;
> Intros m n m_le_n m_not_n;
> Refine LeE m n;
> Refine m_le_n;
> Intros p p_plus_m_is_n;
> Refine zero_or_succ' p;
> 2 Intros p_is_zero;
> Refine NotE';
> 2 Refine m_not_n;
> Refine transl;
> Refine p_plus_m_is_n;
> Refine trans;
> Refine zero_plus;
> Refine wd nat nat [z : Nat] plus z m;
> Refine p_is_zero;
> ReturnAll;
> Intros q p_is_Sq;
> Refine LtI;
> Refine transl;
> Refine p_plus_m_is_n;
> Refine wd nat nat ([z : Nat] plus z m) p (succ q);
> Refine p_is_Sq;
> ReturnAll;
> Le_Neq_Lt;

> Claim Le_LtS : (m, n : Nat) Le m n -> Lt m (succ n);
> Intros m n;
> Refine LeE;
> Intros p p_plus_m_is_n;
> Refine LtI;
> Refine trans;
> Refine wd nat nat succ (plus p m);
> Refine p_plus_m_is_n;
> Refine sym;
> Refine succ_plus;
> ReturnAll;
> Le_LtS;

> Claim LtS_Le : (m, n : Nat) Lt m (succ n) -> Le m n;
> Intros m n;
> Refine LtE;
> Intros p Sp_plus_m_is_Sn;
> Refine LeI;
> Refine Peano3;
> Refine trans;
> 2 Refine succ_plus;
> Refine Sp_plus_m_is_Sn;
> ReturnAll;
> LtS_Le;

> Claim Lt_SLe : (m, n : Nat) Lt m n -> Le (succ m) n;
> Intros m n;
> Refine LtE;
> Intros p Spm_is_n;
> Refine LeI;
> 2 Refine p;
> Refine trans;
> Refine Spm_is_n;
> Refine succ_plus;
> ReturnAll;
> Lt_SLe;

> Claim SLe_Lt : (m, n : Nat) Le (succ m) n -> Lt m n;
> Intros m n;
> Refine LeE;
> Intros p pSm_is_n;
> Refine LtI;
> 2 Refine p;
> Refine trans;
> Refine pSm_is_n;
> Refine sym;
> Refine succ_plus;
> ReturnAll;
> SLe_Lt;

> Claim Lt_Le_trans : (m, n, p : Nat) Lt m n -> Le n p -> Lt m p;
> Intros m n p m_lt_n;
> Refine LeE;
> Intros x x_plus_n_is_p;
> Refine LtE;
> Refine m_lt_n;
> Intros y Sy_plus_m_is_n;
> Refine LtI;
> 2 Refine (plus x y);
> Refine trans;
> Refine x_plus_n_is_p;
> Refine trans;
> Refine wd nat nat (plus x) ? ? Sy_plus_m_is_n;
> Refine plus_assocr x (succ y) m;
> ReturnAll;
> Lt_Le_trans;

> Claim Le_Lt_trans : (m, n, p : Nat) Le m n -> Lt n p -> Lt m p;
> Intros m n p m_le_n;
> Refine LtE;
> Intros k kn_is_p;
> Refine LeE;
> Refine m_le_n;
> Intros k' km_is_n;
> Refine LtI;
> 2 Refine (plus k k');
> Refine EqE nat ([z : Nat] Eq nat (plus z m) p) (plus (succ k) k') (succ (plus k k'));
> Refine sym;
> Refine succ_plus k k';
> Refine trans nat ? (plus (succ k) (plus k' m));
> Refine EqE' nat ([z : Nat] Eq nat (plus (succ k) z) p) ? ? km_is_n;
> Refine kn_is_p;
> Refine plus_assocr;
> ReturnAll;
> Le_Lt_trans;

> Claim Lt_or_Le : (m, n : Nat) Or (Lt m n) (Le n m);
> Intros m n;
> Refine trichotomy' m n;
> Intros n_lt_m;
> Refine OrI2;
> Refine Lt_Le;
> Refine n_lt_m;
> ReturnAll;
> Intros m_is_n;
> Refine OrI2;
> Refine Eq_Le;
> Refine sym;
> Refine m_is_n;
> ReturnAll;
> Refine OrI1;
> ReturnAll;
> Lt_or_Le;

> Claim Le_times_cancelr : (m, n, p : Nat) Le (times m p) (times n p) -> Neq nat p zero -> Le m n;
> Intros m n p mp_le_np p_not_zero;
> Refine OrE;
> Refine Le_Lt_or_eq (times m p) (times n p);
> Refine mp_le_np;
> Intros mp_is_np;
> Refine Eq_Le;
> Refine times_cancelr;
> Refine p_not_zero;
> Refine mp_is_np;
> ReturnAll;
> Intros mp_lt_np;
> Refine Lt_Le;
> Refine Lt_times_cancelr;
> Refine mp_lt_np;
> ReturnAll;
> Le_times_cancelr;

> Claim Le_times_cancell : (m, n, p : Nat) Le (times m n) (times m p) -> Neq nat m zero -> Le n p;
> Intros m n p mn_le_mp m_not_zero;
> Refine Le_times_cancelr n p m;
> Refine m_not_zero;
> Refine EqE2 nat nat Le;
> Refine mn_le_mp;
> Refine times_comm;
> Refine times_comm;
> ReturnAll;
> Le_times_cancell;