type-natural 0.7.1.0 → 0.7.1.1

- Data.Type.Natural: (%:**) :: forall (t_aYIR :: Nat) (t_aYIS :: Nat). Sing t_aYIR -> Sing t_aYIS -> Sing (Apply (Apply (:**$) t_aYIR) t_aYIS :: Nat)

- Data.Type.Natural: class (SDecide nat, SNum nat, SEnum nat, nat ~ nat) => IsPeano nat where succInj' _ _ = succInj plusMinus' n m = start (n %:+ m %:- n) === m %:+ n %:- n `because` minusCongL (plusComm n m) n === m `because` plusMinus m n plusZeroL sn = idLProof (induction base step sn) where base :: PlusZeroL (Zero nat) base = IdentityL (plusZeroR sZero) step :: Sing (n :: nat) -> PlusZeroL n -> PlusZeroL (S n) step sk (IdentityL ih) = IdentityL $ start (sZero %:+ sS sk) === sS (sZero %:+ sk) `because` plusSuccR sZero sk === sS sk `because` succCong ih plusSuccL sn0 sm0 = plusSuccLProof (induction base step sm0) sn0 where base :: PlusSuccL (Zero nat) base = PlusSuccL $ \ sn -> start (sS sn %:+ sZero) === sS sn `because` plusZeroR (sS sn) === sS (sn %:+ sZero) `because` succCong (sym $ plusZeroR sn) step :: Sing (n :: nat) -> PlusSuccL n -> PlusSuccL (S n) step sm (PlusSuccL ih) = PlusSuccL $ \ sn -> start (sS sn %:+ sS sm) === sS (sS sn %:+ sm) `because` plusSuccR (sS sn) sm === sS (sS (sn %:+ sm)) `because` succCong (ih sn) === sS (sn %:+ sS sm) `because` succCong (sym $ plusSuccR sn sm) plusZeroR sn = idRProof (induction base step sn) where base :: PlusZeroR (Zero nat) base = IdentityR (plusZeroL sZero) step :: Sing (n :: nat) -> PlusZeroR n -> PlusZeroR (S n) step sk (IdentityR ih) = IdentityR $ start (sS sk %:+ sZero) === sS (sk %:+ sZero) `because` plusSuccL sk sZero === sS sk `because` succCong ih plusSuccR sn0 = plusSuccRProof (induction base step sn0) where base :: PlusSuccR (Zero nat) base = PlusSuccR $ \ sk -> start (sZero %:+ sS sk) === sS sk `because` plusZeroL (sS sk) === sS (sZero %:+ sk) `because` succCong (sym $ plusZeroL sk) step :: Sing (n :: nat) -> PlusSuccR n -> PlusSuccR (S n) step sn (PlusSuccR ih) = PlusSuccR $ \ sk -> start (sS sn %:+ sS sk) === sS (sn %:+ sS sk) `because` plusSuccL sn (sS sk) === sS (sS (sn %:+ sk)) `because` succCong (ih sk) === sS (sS sn %:+ sk) `because` succCong (sym $ plusSuccL sn sk) plusComm sn0 = commProof (induction base step sn0) where base :: PlusComm (Zero nat) base = Comm $ \ sk -> start (sZero %:+ sk) === sk `because` plusZeroL sk === (sk %:+ sZero) `because` sym (plusZeroR sk) step :: Sing (n :: nat) -> PlusComm n -> PlusComm (S n) step sn (Comm ih) = Comm $ \ sk -> start (sS sn %:+ sk) === sS (sn %:+ sk) `because` plusSuccL sn sk === sS (sk %:+ sn) `because` succCong (ih sk) === sk %:+ sS sn `because` sym (plusSuccR sk sn) plusAssoc sn m l = assocProof (induction base step sn) m l where base :: Assoc (:+$$) (Zero nat) base = Assoc $ \ sk sl -> start ((sZero %:+ sk) %:+ sl) === sk %:+ sl `because` plusCongL (plusZeroL sk) sl === (sZero %:+ (sk %:+ sl)) `because` sym (plusZeroL (sk %:+ sl)) step :: forall k. Sing (k :: nat) -> Assoc (:+$$) k -> Assoc (:+$$) (S k) step sk (Assoc ih) = Assoc $ \ sl su -> start ((sS sk %:+ sl) %:+ su) === (sS (sk %:+ sl) %:+ su) `because` plusCongL (plusSuccL sk sl) su === sS (sk %:+ sl %:+ su) `because` plusSuccL (sk %:+ sl) su === sS (sk %:+ (sl %:+ su)) `because` succCong (ih sl su) === sS sk %:+ (sl %:+ su) `because` sym (plusSuccL sk (sl %:+ su)) multZeroL sn0 = multZeroLProof $ induction base step sn0 where base :: MultZeroL (Zero nat) base = MultZeroL (multZeroR sZero) step :: Sing (k :: nat) -> MultZeroL k -> MultZeroL (S k) step sk (MultZeroL ih) = MultZeroL $ start (sZero %:* sS sk) === sZero %:* sk %:+ sZero `because` multSuccR sZero sk === sZero %:* sk `because` plusZeroR (sZero %:* sk) === sZero `because` ih multSuccL sn0 sm0 = multSuccLProof (induction base step sm0) sn0 where base :: MultSuccL (Zero nat) base = MultSuccL $ \ sk -> start (sS sk %:* sZero) === sZero `because` multZeroR (sS sk) === sk %:* sZero `because` sym (multZeroR sk) === sk %:* sZero %:+ sZero `because` sym (plusZeroR (sk %:* sZero)) step :: Sing (m :: nat) -> MultSuccL m -> MultSuccL (S m) step sm (MultSuccL ih) = MultSuccL $ \ sk -> start (sS sk %:* sS sm) === sS sk %:* sm %:+ sS sk `because` multSuccR (sS sk) sm === (sk %:* sm %:+ sm) %:+ sS sk `because` plusCongL (ih sk) (sS sk) === sS ((sk %:* sm %:+ sm) %:+ sk) `because` plusSuccR (sk %:* sm %:+ sm) sk === sS (sk %:* sm %:+ (sm %:+ sk)) `because` succCong (plusAssoc (sk %:* sm) sm sk) === sS (sk %:* sm %:+ (sk %:+ sm)) `because` succCong (plusCongR (sk %:* sm) (plusComm sm sk)) === sS ((sk %:* sm %:+ sk) %:+ sm) `because` succCong (sym $ plusAssoc (sk %:* sm) sk sm) === sS ((sk %:* sS sm) %:+ sm) `because` succCong (plusCongL (sym $ multSuccR sk sm) sm) === sk %:* sS sm %:+ sS sm `because` sym (plusSuccR (sk %:* sS sm) sm) multZeroR sn0 = multZeroRProof $ induction base step sn0 where base :: MultZeroR (Zero nat) base = MultZeroR (multZeroR sZero) step :: Sing (k :: nat) -> MultZeroR k -> MultZeroR (S k) step sk (MultZeroR ih) = MultZeroR $ start (sS sk %:* sZero) === sk %:* sZero %:+ sZero `because` multSuccL sk sZero === sk %:* sZero `because` plusZeroR (sk %:* sZero) === sZero `because` ih multSuccR sn0 = multSuccRProof $ induction base step sn0 where base :: MultSuccR (Zero nat) base = MultSuccR $ \ sk -> start (sZero %:* sS sk) === sZero `because` multZeroL (sS sk) === sZero %:* sk `because` sym (multZeroL sk) === sZero %:* sk %:+ sZero `because` sym (plusZeroR (sZero %:* sk)) step :: Sing (n :: nat) -> MultSuccR n -> MultSuccR (S n) step sn (MultSuccR ih) = MultSuccR $ \ sk -> start (sS sn %:* sS sk) === sn %:* sS sk %:+ sS sk `because` multSuccL sn (sS sk) === sS (sn %:* sS sk %:+ sk) `because` plusSuccR (sn %:* sS sk) sk === sS (sn %:* sk %:+ sn %:+ sk) `because` succCong (plusCongL (ih sk) sk) === sS (sn %:* sk %:+ (sn %:+ sk)) `because` succCong (plusAssoc (sn %:* sk) sn sk) === sS (sn %:* sk %:+ (sk %:+ sn)) `because` succCong (plusCongR (sn %:* sk) (plusComm sn sk)) === sS (sn %:* sk %:+ sk %:+ sn) `because` succCong (sym $ plusAssoc (sn %:* sk) sk sn) === sS (sS sn %:* sk %:+ sn) `because` succCong (plusCongL (sym $ multSuccL sn sk) sn) === sS sn %:* sk %:+ sS sn `because` sym (plusSuccR (sS sn %:* sk) sn) multComm sn0 = commProof (induction base step sn0) where base :: Comm (:*$$) (Zero nat) base = Comm $ \ sk -> start (sZero %:* sk) === sZero `because` multZeroL sk === sk %:* sZero `because` sym (multZeroR sk) step :: Sing (n :: nat) -> Comm (:*$$) n -> Comm (:*$$) (S n) step sn (Comm ih) = Comm $ \ sk -> start (sS sn %:* sk) === sn %:* sk %:+ sk `because` multSuccL sn sk === sk %:* sn %:+ sk `because` plusCongL (ih sk) sk === sk %:* sS sn `because` sym (multSuccR sk sn) multOneR sn = start (sn %:* sOne) === sn %:* sS sZero `because` multCongR sn (sym $ succOneCong) === sn %:* sZero %:+ sn `because` multSuccR sn sZero === sZero %:+ sn `because` plusCongL (multZeroR sn) sn === sn `because` plusZeroL sn multOneL sn = start (sOne %:* sn) === sn %:* sOne `because` multComm sOne sn === sn `because` multOneR sn plusMultDistrib sn0 = plusMultDistribProof $ induction base step sn0 where base :: PlusMultDistrib (Zero nat) base = PlusMultDistrib $ \ sk sl -> start ((sZero %:+ sk) %:* sl) === (sk %:* sl) `because` multCongL (plusZeroL sk) sl === sZero %:+ (sk %:* sl) `because` sym (plusZeroL (sk %:* sl)) === sZero %:* sl %:+ sk %:* sl `because` plusCongL (sym $ multZeroL sl) (sk %:* sl) step :: Sing (n :: nat) -> PlusMultDistrib n -> PlusMultDistrib (S n) step sn (PlusMultDistrib ih) = PlusMultDistrib $ \ sk sl -> start ((sS sn %:+ sk) %:* sl) === (sS (sn %:+ sk) %:* sl) `because` multCongL (plusSuccL sn sk) sl === (sn %:+ sk) %:* sl %:+ sl `because` multSuccL (sn %:+ sk) sl === (sn %:* sl %:+ sk %:* sl) %:+ sl `because` plusCongL (ih sk sl) sl === sn %:* sl %:+ (sk %:* sl %:+ sl) `because` plusAssoc (sn %:* sl) (sk %:* sl) sl === sn %:* sl %:+ (sl %:+ sk %:* sl) `because` plusCongR (sn %:* sl) (plusComm (sk %:* sl) sl) === (sn %:* sl %:+ sl) %:+ sk %:* sl `because` sym (plusAssoc (sn %:* sl) sl (sk %:* sl)) === (sS sn %:* sl) %:+ sk %:* sl `because` plusCongL (sym $ multSuccL sn sl) (sk %:* sl) multPlusDistrib n m l = start (n %:* (m %:+ l)) === (m %:+ l) %:* n `because` multComm n (m %:+ l) === m %:* n %:+ l %:* n `because` plusMultDistrib m l n === n %:* m %:+ n %:* l `because` plusCong (multComm m n) (multComm l n) minusNilpotent n = start (n %:- n) === (sZero %:+ n) %:- n `because` minusCongL (sym $ plusZeroL n) n === sZero `because` plusMinus sZero n multAssoc sn0 = assocProof $ induction base step sn0 where base :: Assoc (:*$$) (Zero nat) base = Assoc $ \ m l -> start (sZero %:* m %:* l) === sZero %:* l `because` multCongL (multZeroL m) l === sZero `because` multZeroL l === sZero %:* (m %:* l) `because` sym (multZeroL (m %:* l)) step :: Sing (n :: nat) -> Assoc (:*$$) n -> Assoc (:*$$) (S n) step n _ = Assoc $ \ m l -> start (sS n %:* m %:* l) === (n %:* m %:+ m) %:* l `because` multCongL (multSuccL n m) l === n %:* m %:* l %:+ m %:* l `because` plusMultDistrib (n %:* m) m l === n %:* (m %:* l) %:+ m %:* l `because` plusCongL (multAssoc n m l) (m %:* l) === sS n %:* (m %:* l) `because` sym (multSuccL n (m %:* l)) plusEqCancelL = plusEqCancelLProof . induction base step where base :: PlusEqCancelL (Zero nat) base = PlusEqCancelL $ \ l m nlnm -> start l === sZero %:+ l `because` sym (plusZeroL l) === sZero %:+ m `because` nlnm === m `because` plusZeroL m step :: Sing (n :: nat) -> PlusEqCancelL n -> PlusEqCancelL (Succ n) step n (PlusEqCancelL ih) = PlusEqCancelL $ \ l m snlsnm -> succInj $ ih (sS l) (sS m) $ start (n %:+ sS l) === sS (n %:+ l) `because` plusSuccR n l === sS n %:+ l `because` sym (plusSuccL n l) === sS n %:+ m `because` snlsnm === sS (n %:+ m) `because` plusSuccL n m === n %:+ sS m `because` sym (plusSuccR n m) plusEqCancelR n m l nlml = plusEqCancelL l n m $ start (l %:+ n) === (n %:+ l) `because` plusComm l n === (m %:+ l) `because` nlml === (l %:+ m) `because` plusComm m l succAndPlusOneL = proofSuccPlusL . induction base step where base :: SuccPlusL (Zero nat) base = SuccPlusL $ start (sSucc sZero) === sOne `because` succOneCong === sOne %:+ sZero `because` sym (plusZeroR sOne) step :: Sing (n :: nat) -> SuccPlusL n -> SuccPlusL (Succ n) step sn (SuccPlusL ih) = SuccPlusL $ start (sSucc (sSucc sn)) === sSucc (sOne %:+ sn) `because` succCong ih === sOne %:+ sSucc sn `because` sym (plusSuccR sOne sn) succAndPlusOneR n = start (sSucc n) === sOne %:+ n `because` succAndPlusOneL n === n %:+ sOne `because` plusComm sOne n zeroOrSucc = induction base step where base = IsZero step sn _ = IsSucc sn plusEqZeroL n m Refl = case zeroOrSucc n of { IsZero -> Refl IsSucc pn -> absurd $ succNonCyclic (pn %:+ m) (sym $ plusSuccL pn m) } plusEqZeroR n m = plusEqZeroL m n . trans (plusComm m n) predUnique n m snEm = start n === (sPred (sSucc n)) `because` sym (predSucc n) === sPred m `because` predCong snEm multEqSuccElimL n m l nmEsl = case zeroOrSucc n of { IsZero -> absurd $ succNonCyclic l $ sym $ start sZero === sZero %:* m `because` sym (multZeroL m) === sSucc l `because` nmEsl IsSucc pn -> succCong (predUnique pn n Refl) } multEqSuccElimR n m l nmEsl = multEqSuccElimL m n l (multComm m n `trans` nmEsl) minusZero n = start (n %:- sZero) === (n %:+ sZero) %:- sZero `because` minusCongL (sym $ plusZeroR n) sZero === n `because` plusMinus n sZero multEqCancelR = proofMultEqCancelR . induction base step where base :: MultEqCancelR (Zero nat) base = MultEqCancelR $ \ m l zslmsl -> sym $ plusEqZeroR (m %:* l) m $ sym $ start sZero === sZero %:* l `because` sym (multZeroL l) === sZero %:* l %:+ sZero `because` sym (plusZeroR (sZero %:* l)) === sZero %:* sSucc l `because` sym (multSuccR sZero l) === m %:* sSucc l `because` zslmsl === m %:* l %:+ m `because` multSuccR m l step :: Sing (n :: nat) -> MultEqCancelR n -> MultEqCancelR (Succ n) step n (MultEqCancelR ih) = MultEqCancelR $ \ m l snmssnl -> let m' = sPred m pf = start (m %:* sSucc l) === sSucc n %:* sSucc l `because` sym snmssnl === n %:* sSucc l %:+ sSucc l `because` multSuccL n (sSucc l) === sSucc (n %:* sSucc l %:+ l) `because` plusSuccR (n %:* sSucc l) l sm'Em = multEqSuccElimL m (sSucc l) (n %:* sSucc l %:+ l) pf pf' = ih m' l $ plusEqCancelR (n %:* sSucc l) (m' %:* sSucc l) (sSucc l) $ start (n %:* sSucc l %:+ sSucc l) === sSucc (n %:* sSucc l %:+ l) `because` plusSuccR (n %:* sSucc l) l === m %:* sSucc l `because` sym pf === sSucc m' %:* sSucc l `because` multCongL sm'Em (sSucc l) === (m' %:* sSucc l %:+ sSucc l) `because` multSuccL m' (sSucc l) in succCong pf' `trans` sym sm'Em succPred n nonZero = case zeroOrSucc n of { IsZero -> absurd $ nonZero Refl IsSucc n' -> sym $ succCong $ predUnique n' n Refl } multEqCancelL n m l snmEsnl = multEqCancelR m l n $ multComm m (sSucc n) `trans` snmEsnl `trans` multComm (sSucc n) l sPred' pxy sn = coerce (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn)

- Data.Type.Natural: data SSym0 (l_aVSX :: TyFun Nat Nat)

- Data.Type.Natural: type SSym1 (t_aVSW :: Nat) = S t_aVSW

- Data.Type.Natural.Builtin: class (SDecide nat, SNum nat, SEnum nat, nat ~ nat) => IsPeano nat where succInj' _ _ = succInj plusMinus' n m = start (n %:+ m %:- n) === m %:+ n %:- n `because` minusCongL (plusComm n m) n === m `because` plusMinus m n plusZeroL sn = idLProof (induction base step sn) where base :: PlusZeroL (Zero nat) base = IdentityL (plusZeroR sZero) step :: Sing (n :: nat) -> PlusZeroL n -> PlusZeroL (S n) step sk (IdentityL ih) = IdentityL $ start (sZero %:+ sS sk) === sS (sZero %:+ sk) `because` plusSuccR sZero sk === sS sk `because` succCong ih plusSuccL sn0 sm0 = plusSuccLProof (induction base step sm0) sn0 where base :: PlusSuccL (Zero nat) base = PlusSuccL $ \ sn -> start (sS sn %:+ sZero) === sS sn `because` plusZeroR (sS sn) === sS (sn %:+ sZero) `because` succCong (sym $ plusZeroR sn) step :: Sing (n :: nat) -> PlusSuccL n -> PlusSuccL (S n) step sm (PlusSuccL ih) = PlusSuccL $ \ sn -> start (sS sn %:+ sS sm) === sS (sS sn %:+ sm) `because` plusSuccR (sS sn) sm === sS (sS (sn %:+ sm)) `because` succCong (ih sn) === sS (sn %:+ sS sm) `because` succCong (sym $ plusSuccR sn sm) plusZeroR sn = idRProof (induction base step sn) where base :: PlusZeroR (Zero nat) base = IdentityR (plusZeroL sZero) step :: Sing (n :: nat) -> PlusZeroR n -> PlusZeroR (S n) step sk (IdentityR ih) = IdentityR $ start (sS sk %:+ sZero) === sS (sk %:+ sZero) `because` plusSuccL sk sZero === sS sk `because` succCong ih plusSuccR sn0 = plusSuccRProof (induction base step sn0) where base :: PlusSuccR (Zero nat) base = PlusSuccR $ \ sk -> start (sZero %:+ sS sk) === sS sk `because` plusZeroL (sS sk) === sS (sZero %:+ sk) `because` succCong (sym $ plusZeroL sk) step :: Sing (n :: nat) -> PlusSuccR n -> PlusSuccR (S n) step sn (PlusSuccR ih) = PlusSuccR $ \ sk -> start (sS sn %:+ sS sk) === sS (sn %:+ sS sk) `because` plusSuccL sn (sS sk) === sS (sS (sn %:+ sk)) `because` succCong (ih sk) === sS (sS sn %:+ sk) `because` succCong (sym $ plusSuccL sn sk) plusComm sn0 = commProof (induction base step sn0) where base :: PlusComm (Zero nat) base = Comm $ \ sk -> start (sZero %:+ sk) === sk `because` plusZeroL sk === (sk %:+ sZero) `because` sym (plusZeroR sk) step :: Sing (n :: nat) -> PlusComm n -> PlusComm (S n) step sn (Comm ih) = Comm $ \ sk -> start (sS sn %:+ sk) === sS (sn %:+ sk) `because` plusSuccL sn sk === sS (sk %:+ sn) `because` succCong (ih sk) === sk %:+ sS sn `because` sym (plusSuccR sk sn) plusAssoc sn m l = assocProof (induction base step sn) m l where base :: Assoc (:+$$) (Zero nat) base = Assoc $ \ sk sl -> start ((sZero %:+ sk) %:+ sl) === sk %:+ sl `because` plusCongL (plusZeroL sk) sl === (sZero %:+ (sk %:+ sl)) `because` sym (plusZeroL (sk %:+ sl)) step :: forall k. Sing (k :: nat) -> Assoc (:+$$) k -> Assoc (:+$$) (S k) step sk (Assoc ih) = Assoc $ \ sl su -> start ((sS sk %:+ sl) %:+ su) === (sS (sk %:+ sl) %:+ su) `because` plusCongL (plusSuccL sk sl) su === sS (sk %:+ sl %:+ su) `because` plusSuccL (sk %:+ sl) su === sS (sk %:+ (sl %:+ su)) `because` succCong (ih sl su) === sS sk %:+ (sl %:+ su) `because` sym (plusSuccL sk (sl %:+ su)) multZeroL sn0 = multZeroLProof $ induction base step sn0 where base :: MultZeroL (Zero nat) base = MultZeroL (multZeroR sZero) step :: Sing (k :: nat) -> MultZeroL k -> MultZeroL (S k) step sk (MultZeroL ih) = MultZeroL $ start (sZero %:* sS sk) === sZero %:* sk %:+ sZero `because` multSuccR sZero sk === sZero %:* sk `because` plusZeroR (sZero %:* sk) === sZero `because` ih multSuccL sn0 sm0 = multSuccLProof (induction base step sm0) sn0 where base :: MultSuccL (Zero nat) base = MultSuccL $ \ sk -> start (sS sk %:* sZero) === sZero `because` multZeroR (sS sk) === sk %:* sZero `because` sym (multZeroR sk) === sk %:* sZero %:+ sZero `because` sym (plusZeroR (sk %:* sZero)) step :: Sing (m :: nat) -> MultSuccL m -> MultSuccL (S m) step sm (MultSuccL ih) = MultSuccL $ \ sk -> start (sS sk %:* sS sm) === sS sk %:* sm %:+ sS sk `because` multSuccR (sS sk) sm === (sk %:* sm %:+ sm) %:+ sS sk `because` plusCongL (ih sk) (sS sk) === sS ((sk %:* sm %:+ sm) %:+ sk) `because` plusSuccR (sk %:* sm %:+ sm) sk === sS (sk %:* sm %:+ (sm %:+ sk)) `because` succCong (plusAssoc (sk %:* sm) sm sk) === sS (sk %:* sm %:+ (sk %:+ sm)) `because` succCong (plusCongR (sk %:* sm) (plusComm sm sk)) === sS ((sk %:* sm %:+ sk) %:+ sm) `because` succCong (sym $ plusAssoc (sk %:* sm) sk sm) === sS ((sk %:* sS sm) %:+ sm) `because` succCong (plusCongL (sym $ multSuccR sk sm) sm) === sk %:* sS sm %:+ sS sm `because` sym (plusSuccR (sk %:* sS sm) sm) multZeroR sn0 = multZeroRProof $ induction base step sn0 where base :: MultZeroR (Zero nat) base = MultZeroR (multZeroR sZero) step :: Sing (k :: nat) -> MultZeroR k -> MultZeroR (S k) step sk (MultZeroR ih) = MultZeroR $ start (sS sk %:* sZero) === sk %:* sZero %:+ sZero `because` multSuccL sk sZero === sk %:* sZero `because` plusZeroR (sk %:* sZero) === sZero `because` ih multSuccR sn0 = multSuccRProof $ induction base step sn0 where base :: MultSuccR (Zero nat) base = MultSuccR $ \ sk -> start (sZero %:* sS sk) === sZero `because` multZeroL (sS sk) === sZero %:* sk `because` sym (multZeroL sk) === sZero %:* sk %:+ sZero `because` sym (plusZeroR (sZero %:* sk)) step :: Sing (n :: nat) -> MultSuccR n -> MultSuccR (S n) step sn (MultSuccR ih) = MultSuccR $ \ sk -> start (sS sn %:* sS sk) === sn %:* sS sk %:+ sS sk `because` multSuccL sn (sS sk) === sS (sn %:* sS sk %:+ sk) `because` plusSuccR (sn %:* sS sk) sk === sS (sn %:* sk %:+ sn %:+ sk) `because` succCong (plusCongL (ih sk) sk) === sS (sn %:* sk %:+ (sn %:+ sk)) `because` succCong (plusAssoc (sn %:* sk) sn sk) === sS (sn %:* sk %:+ (sk %:+ sn)) `because` succCong (plusCongR (sn %:* sk) (plusComm sn sk)) === sS (sn %:* sk %:+ sk %:+ sn) `because` succCong (sym $ plusAssoc (sn %:* sk) sk sn) === sS (sS sn %:* sk %:+ sn) `because` succCong (plusCongL (sym $ multSuccL sn sk) sn) === sS sn %:* sk %:+ sS sn `because` sym (plusSuccR (sS sn %:* sk) sn) multComm sn0 = commProof (induction base step sn0) where base :: Comm (:*$$) (Zero nat) base = Comm $ \ sk -> start (sZero %:* sk) === sZero `because` multZeroL sk === sk %:* sZero `because` sym (multZeroR sk) step :: Sing (n :: nat) -> Comm (:*$$) n -> Comm (:*$$) (S n) step sn (Comm ih) = Comm $ \ sk -> start (sS sn %:* sk) === sn %:* sk %:+ sk `because` multSuccL sn sk === sk %:* sn %:+ sk `because` plusCongL (ih sk) sk === sk %:* sS sn `because` sym (multSuccR sk sn) multOneR sn = start (sn %:* sOne) === sn %:* sS sZero `because` multCongR sn (sym $ succOneCong) === sn %:* sZero %:+ sn `because` multSuccR sn sZero === sZero %:+ sn `because` plusCongL (multZeroR sn) sn === sn `because` plusZeroL sn multOneL sn = start (sOne %:* sn) === sn %:* sOne `because` multComm sOne sn === sn `because` multOneR sn plusMultDistrib sn0 = plusMultDistribProof $ induction base step sn0 where base :: PlusMultDistrib (Zero nat) base = PlusMultDistrib $ \ sk sl -> start ((sZero %:+ sk) %:* sl) === (sk %:* sl) `because` multCongL (plusZeroL sk) sl === sZero %:+ (sk %:* sl) `because` sym (plusZeroL (sk %:* sl)) === sZero %:* sl %:+ sk %:* sl `because` plusCongL (sym $ multZeroL sl) (sk %:* sl) step :: Sing (n :: nat) -> PlusMultDistrib n -> PlusMultDistrib (S n) step sn (PlusMultDistrib ih) = PlusMultDistrib $ \ sk sl -> start ((sS sn %:+ sk) %:* sl) === (sS (sn %:+ sk) %:* sl) `because` multCongL (plusSuccL sn sk) sl === (sn %:+ sk) %:* sl %:+ sl `because` multSuccL (sn %:+ sk) sl === (sn %:* sl %:+ sk %:* sl) %:+ sl `because` plusCongL (ih sk sl) sl === sn %:* sl %:+ (sk %:* sl %:+ sl) `because` plusAssoc (sn %:* sl) (sk %:* sl) sl === sn %:* sl %:+ (sl %:+ sk %:* sl) `because` plusCongR (sn %:* sl) (plusComm (sk %:* sl) sl) === (sn %:* sl %:+ sl) %:+ sk %:* sl `because` sym (plusAssoc (sn %:* sl) sl (sk %:* sl)) === (sS sn %:* sl) %:+ sk %:* sl `because` plusCongL (sym $ multSuccL sn sl) (sk %:* sl) multPlusDistrib n m l = start (n %:* (m %:+ l)) === (m %:+ l) %:* n `because` multComm n (m %:+ l) === m %:* n %:+ l %:* n `because` plusMultDistrib m l n === n %:* m %:+ n %:* l `because` plusCong (multComm m n) (multComm l n) minusNilpotent n = start (n %:- n) === (sZero %:+ n) %:- n `because` minusCongL (sym $ plusZeroL n) n === sZero `because` plusMinus sZero n multAssoc sn0 = assocProof $ induction base step sn0 where base :: Assoc (:*$$) (Zero nat) base = Assoc $ \ m l -> start (sZero %:* m %:* l) === sZero %:* l `because` multCongL (multZeroL m) l === sZero `because` multZeroL l === sZero %:* (m %:* l) `because` sym (multZeroL (m %:* l)) step :: Sing (n :: nat) -> Assoc (:*$$) n -> Assoc (:*$$) (S n) step n _ = Assoc $ \ m l -> start (sS n %:* m %:* l) === (n %:* m %:+ m) %:* l `because` multCongL (multSuccL n m) l === n %:* m %:* l %:+ m %:* l `because` plusMultDistrib (n %:* m) m l === n %:* (m %:* l) %:+ m %:* l `because` plusCongL (multAssoc n m l) (m %:* l) === sS n %:* (m %:* l) `because` sym (multSuccL n (m %:* l)) plusEqCancelL = plusEqCancelLProof . induction base step where base :: PlusEqCancelL (Zero nat) base = PlusEqCancelL $ \ l m nlnm -> start l === sZero %:+ l `because` sym (plusZeroL l) === sZero %:+ m `because` nlnm === m `because` plusZeroL m step :: Sing (n :: nat) -> PlusEqCancelL n -> PlusEqCancelL (Succ n) step n (PlusEqCancelL ih) = PlusEqCancelL $ \ l m snlsnm -> succInj $ ih (sS l) (sS m) $ start (n %:+ sS l) === sS (n %:+ l) `because` plusSuccR n l === sS n %:+ l `because` sym (plusSuccL n l) === sS n %:+ m `because` snlsnm === sS (n %:+ m) `because` plusSuccL n m === n %:+ sS m `because` sym (plusSuccR n m) plusEqCancelR n m l nlml = plusEqCancelL l n m $ start (l %:+ n) === (n %:+ l) `because` plusComm l n === (m %:+ l) `because` nlml === (l %:+ m) `because` plusComm m l succAndPlusOneL = proofSuccPlusL . induction base step where base :: SuccPlusL (Zero nat) base = SuccPlusL $ start (sSucc sZero) === sOne `because` succOneCong === sOne %:+ sZero `because` sym (plusZeroR sOne) step :: Sing (n :: nat) -> SuccPlusL n -> SuccPlusL (Succ n) step sn (SuccPlusL ih) = SuccPlusL $ start (sSucc (sSucc sn)) === sSucc (sOne %:+ sn) `because` succCong ih === sOne %:+ sSucc sn `because` sym (plusSuccR sOne sn) succAndPlusOneR n = start (sSucc n) === sOne %:+ n `because` succAndPlusOneL n === n %:+ sOne `because` plusComm sOne n zeroOrSucc = induction base step where base = IsZero step sn _ = IsSucc sn plusEqZeroL n m Refl = case zeroOrSucc n of { IsZero -> Refl IsSucc pn -> absurd $ succNonCyclic (pn %:+ m) (sym $ plusSuccL pn m) } plusEqZeroR n m = plusEqZeroL m n . trans (plusComm m n) predUnique n m snEm = start n === (sPred (sSucc n)) `because` sym (predSucc n) === sPred m `because` predCong snEm multEqSuccElimL n m l nmEsl = case zeroOrSucc n of { IsZero -> absurd $ succNonCyclic l $ sym $ start sZero === sZero %:* m `because` sym (multZeroL m) === sSucc l `because` nmEsl IsSucc pn -> succCong (predUnique pn n Refl) } multEqSuccElimR n m l nmEsl = multEqSuccElimL m n l (multComm m n `trans` nmEsl) minusZero n = start (n %:- sZero) === (n %:+ sZero) %:- sZero `because` minusCongL (sym $ plusZeroR n) sZero === n `because` plusMinus n sZero multEqCancelR = proofMultEqCancelR . induction base step where base :: MultEqCancelR (Zero nat) base = MultEqCancelR $ \ m l zslmsl -> sym $ plusEqZeroR (m %:* l) m $ sym $ start sZero === sZero %:* l `because` sym (multZeroL l) === sZero %:* l %:+ sZero `because` sym (plusZeroR (sZero %:* l)) === sZero %:* sSucc l `because` sym (multSuccR sZero l) === m %:* sSucc l `because` zslmsl === m %:* l %:+ m `because` multSuccR m l step :: Sing (n :: nat) -> MultEqCancelR n -> MultEqCancelR (Succ n) step n (MultEqCancelR ih) = MultEqCancelR $ \ m l snmssnl -> let m' = sPred m pf = start (m %:* sSucc l) === sSucc n %:* sSucc l `because` sym snmssnl === n %:* sSucc l %:+ sSucc l `because` multSuccL n (sSucc l) === sSucc (n %:* sSucc l %:+ l) `because` plusSuccR (n %:* sSucc l) l sm'Em = multEqSuccElimL m (sSucc l) (n %:* sSucc l %:+ l) pf pf' = ih m' l $ plusEqCancelR (n %:* sSucc l) (m' %:* sSucc l) (sSucc l) $ start (n %:* sSucc l %:+ sSucc l) === sSucc (n %:* sSucc l %:+ l) `because` plusSuccR (n %:* sSucc l) l === m %:* sSucc l `because` sym pf === sSucc m' %:* sSucc l `because` multCongL sm'Em (sSucc l) === (m' %:* sSucc l %:+ sSucc l) `because` multSuccL m' (sSucc l) in succCong pf' `trans` sym sm'Em succPred n nonZero = case zeroOrSucc n of { IsZero -> absurd $ nonZero Refl IsSucc n' -> sym $ succCong $ predUnique n' n Refl } multEqCancelL n m l snmEsnl = multEqCancelR m l n $ multComm m (sSucc n) `trans` snmEsnl `trans` multComm (sSucc n) l sPred' pxy sn = coerce (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn)

- Data.Type.Natural.Class.Arithmetic: class (SDecide nat, SNum nat, SEnum nat, nat ~ nat) => IsPeano nat where succInj' _ _ = succInj plusMinus' n m = start (n %:+ m %:- n) === m %:+ n %:- n `because` minusCongL (plusComm n m) n === m `because` plusMinus m n plusZeroL sn = idLProof (induction base step sn) where base :: PlusZeroL (Zero nat) base = IdentityL (plusZeroR sZero) step :: Sing (n :: nat) -> PlusZeroL n -> PlusZeroL (S n) step sk (IdentityL ih) = IdentityL $ start (sZero %:+ sS sk) === sS (sZero %:+ sk) `because` plusSuccR sZero sk === sS sk `because` succCong ih plusSuccL sn0 sm0 = plusSuccLProof (induction base step sm0) sn0 where base :: PlusSuccL (Zero nat) base = PlusSuccL $ \ sn -> start (sS sn %:+ sZero) === sS sn `because` plusZeroR (sS sn) === sS (sn %:+ sZero) `because` succCong (sym $ plusZeroR sn) step :: Sing (n :: nat) -> PlusSuccL n -> PlusSuccL (S n) step sm (PlusSuccL ih) = PlusSuccL $ \ sn -> start (sS sn %:+ sS sm) === sS (sS sn %:+ sm) `because` plusSuccR (sS sn) sm === sS (sS (sn %:+ sm)) `because` succCong (ih sn) === sS (sn %:+ sS sm) `because` succCong (sym $ plusSuccR sn sm) plusZeroR sn = idRProof (induction base step sn) where base :: PlusZeroR (Zero nat) base = IdentityR (plusZeroL sZero) step :: Sing (n :: nat) -> PlusZeroR n -> PlusZeroR (S n) step sk (IdentityR ih) = IdentityR $ start (sS sk %:+ sZero) === sS (sk %:+ sZero) `because` plusSuccL sk sZero === sS sk `because` succCong ih plusSuccR sn0 = plusSuccRProof (induction base step sn0) where base :: PlusSuccR (Zero nat) base = PlusSuccR $ \ sk -> start (sZero %:+ sS sk) === sS sk `because` plusZeroL (sS sk) === sS (sZero %:+ sk) `because` succCong (sym $ plusZeroL sk) step :: Sing (n :: nat) -> PlusSuccR n -> PlusSuccR (S n) step sn (PlusSuccR ih) = PlusSuccR $ \ sk -> start (sS sn %:+ sS sk) === sS (sn %:+ sS sk) `because` plusSuccL sn (sS sk) === sS (sS (sn %:+ sk)) `because` succCong (ih sk) === sS (sS sn %:+ sk) `because` succCong (sym $ plusSuccL sn sk) plusComm sn0 = commProof (induction base step sn0) where base :: PlusComm (Zero nat) base = Comm $ \ sk -> start (sZero %:+ sk) === sk `because` plusZeroL sk === (sk %:+ sZero) `because` sym (plusZeroR sk) step :: Sing (n :: nat) -> PlusComm n -> PlusComm (S n) step sn (Comm ih) = Comm $ \ sk -> start (sS sn %:+ sk) === sS (sn %:+ sk) `because` plusSuccL sn sk === sS (sk %:+ sn) `because` succCong (ih sk) === sk %:+ sS sn `because` sym (plusSuccR sk sn) plusAssoc sn m l = assocProof (induction base step sn) m l where base :: Assoc (:+$$) (Zero nat) base = Assoc $ \ sk sl -> start ((sZero %:+ sk) %:+ sl) === sk %:+ sl `because` plusCongL (plusZeroL sk) sl === (sZero %:+ (sk %:+ sl)) `because` sym (plusZeroL (sk %:+ sl)) step :: forall k. Sing (k :: nat) -> Assoc (:+$$) k -> Assoc (:+$$) (S k) step sk (Assoc ih) = Assoc $ \ sl su -> start ((sS sk %:+ sl) %:+ su) === (sS (sk %:+ sl) %:+ su) `because` plusCongL (plusSuccL sk sl) su === sS (sk %:+ sl %:+ su) `because` plusSuccL (sk %:+ sl) su === sS (sk %:+ (sl %:+ su)) `because` succCong (ih sl su) === sS sk %:+ (sl %:+ su) `because` sym (plusSuccL sk (sl %:+ su)) multZeroL sn0 = multZeroLProof $ induction base step sn0 where base :: MultZeroL (Zero nat) base = MultZeroL (multZeroR sZero) step :: Sing (k :: nat) -> MultZeroL k -> MultZeroL (S k) step sk (MultZeroL ih) = MultZeroL $ start (sZero %:* sS sk) === sZero %:* sk %:+ sZero `because` multSuccR sZero sk === sZero %:* sk `because` plusZeroR (sZero %:* sk) === sZero `because` ih multSuccL sn0 sm0 = multSuccLProof (induction base step sm0) sn0 where base :: MultSuccL (Zero nat) base = MultSuccL $ \ sk -> start (sS sk %:* sZero) === sZero `because` multZeroR (sS sk) === sk %:* sZero `because` sym (multZeroR sk) === sk %:* sZero %:+ sZero `because` sym (plusZeroR (sk %:* sZero)) step :: Sing (m :: nat) -> MultSuccL m -> MultSuccL (S m) step sm (MultSuccL ih) = MultSuccL $ \ sk -> start (sS sk %:* sS sm) === sS sk %:* sm %:+ sS sk `because` multSuccR (sS sk) sm === (sk %:* sm %:+ sm) %:+ sS sk `because` plusCongL (ih sk) (sS sk) === sS ((sk %:* sm %:+ sm) %:+ sk) `because` plusSuccR (sk %:* sm %:+ sm) sk === sS (sk %:* sm %:+ (sm %:+ sk)) `because` succCong (plusAssoc (sk %:* sm) sm sk) === sS (sk %:* sm %:+ (sk %:+ sm)) `because` succCong (plusCongR (sk %:* sm) (plusComm sm sk)) === sS ((sk %:* sm %:+ sk) %:+ sm) `because` succCong (sym $ plusAssoc (sk %:* sm) sk sm) === sS ((sk %:* sS sm) %:+ sm) `because` succCong (plusCongL (sym $ multSuccR sk sm) sm) === sk %:* sS sm %:+ sS sm `because` sym (plusSuccR (sk %:* sS sm) sm) multZeroR sn0 = multZeroRProof $ induction base step sn0 where base :: MultZeroR (Zero nat) base = MultZeroR (multZeroR sZero) step :: Sing (k :: nat) -> MultZeroR k -> MultZeroR (S k) step sk (MultZeroR ih) = MultZeroR $ start (sS sk %:* sZero) === sk %:* sZero %:+ sZero `because` multSuccL sk sZero === sk %:* sZero `because` plusZeroR (sk %:* sZero) === sZero `because` ih multSuccR sn0 = multSuccRProof $ induction base step sn0 where base :: MultSuccR (Zero nat) base = MultSuccR $ \ sk -> start (sZero %:* sS sk) === sZero `because` multZeroL (sS sk) === sZero %:* sk `because` sym (multZeroL sk) === sZero %:* sk %:+ sZero `because` sym (plusZeroR (sZero %:* sk)) step :: Sing (n :: nat) -> MultSuccR n -> MultSuccR (S n) step sn (MultSuccR ih) = MultSuccR $ \ sk -> start (sS sn %:* sS sk) === sn %:* sS sk %:+ sS sk `because` multSuccL sn (sS sk) === sS (sn %:* sS sk %:+ sk) `because` plusSuccR (sn %:* sS sk) sk === sS (sn %:* sk %:+ sn %:+ sk) `because` succCong (plusCongL (ih sk) sk) === sS (sn %:* sk %:+ (sn %:+ sk)) `because` succCong (plusAssoc (sn %:* sk) sn sk) === sS (sn %:* sk %:+ (sk %:+ sn)) `because` succCong (plusCongR (sn %:* sk) (plusComm sn sk)) === sS (sn %:* sk %:+ sk %:+ sn) `because` succCong (sym $ plusAssoc (sn %:* sk) sk sn) === sS (sS sn %:* sk %:+ sn) `because` succCong (plusCongL (sym $ multSuccL sn sk) sn) === sS sn %:* sk %:+ sS sn `because` sym (plusSuccR (sS sn %:* sk) sn) multComm sn0 = commProof (induction base step sn0) where base :: Comm (:*$$) (Zero nat) base = Comm $ \ sk -> start (sZero %:* sk) === sZero `because` multZeroL sk === sk %:* sZero `because` sym (multZeroR sk) step :: Sing (n :: nat) -> Comm (:*$$) n -> Comm (:*$$) (S n) step sn (Comm ih) = Comm $ \ sk -> start (sS sn %:* sk) === sn %:* sk %:+ sk `because` multSuccL sn sk === sk %:* sn %:+ sk `because` plusCongL (ih sk) sk === sk %:* sS sn `because` sym (multSuccR sk sn) multOneR sn = start (sn %:* sOne) === sn %:* sS sZero `because` multCongR sn (sym $ succOneCong) === sn %:* sZero %:+ sn `because` multSuccR sn sZero === sZero %:+ sn `because` plusCongL (multZeroR sn) sn === sn `because` plusZeroL sn multOneL sn = start (sOne %:* sn) === sn %:* sOne `because` multComm sOne sn === sn `because` multOneR sn plusMultDistrib sn0 = plusMultDistribProof $ induction base step sn0 where base :: PlusMultDistrib (Zero nat) base = PlusMultDistrib $ \ sk sl -> start ((sZero %:+ sk) %:* sl) === (sk %:* sl) `because` multCongL (plusZeroL sk) sl === sZero %:+ (sk %:* sl) `because` sym (plusZeroL (sk %:* sl)) === sZero %:* sl %:+ sk %:* sl `because` plusCongL (sym $ multZeroL sl) (sk %:* sl) step :: Sing (n :: nat) -> PlusMultDistrib n -> PlusMultDistrib (S n) step sn (PlusMultDistrib ih) = PlusMultDistrib $ \ sk sl -> start ((sS sn %:+ sk) %:* sl) === (sS (sn %:+ sk) %:* sl) `because` multCongL (plusSuccL sn sk) sl === (sn %:+ sk) %:* sl %:+ sl `because` multSuccL (sn %:+ sk) sl === (sn %:* sl %:+ sk %:* sl) %:+ sl `because` plusCongL (ih sk sl) sl === sn %:* sl %:+ (sk %:* sl %:+ sl) `because` plusAssoc (sn %:* sl) (sk %:* sl) sl === sn %:* sl %:+ (sl %:+ sk %:* sl) `because` plusCongR (sn %:* sl) (plusComm (sk %:* sl) sl) === (sn %:* sl %:+ sl) %:+ sk %:* sl `because` sym (plusAssoc (sn %:* sl) sl (sk %:* sl)) === (sS sn %:* sl) %:+ sk %:* sl `because` plusCongL (sym $ multSuccL sn sl) (sk %:* sl) multPlusDistrib n m l = start (n %:* (m %:+ l)) === (m %:+ l) %:* n `because` multComm n (m %:+ l) === m %:* n %:+ l %:* n `because` plusMultDistrib m l n === n %:* m %:+ n %:* l `because` plusCong (multComm m n) (multComm l n) minusNilpotent n = start (n %:- n) === (sZero %:+ n) %:- n `because` minusCongL (sym $ plusZeroL n) n === sZero `because` plusMinus sZero n multAssoc sn0 = assocProof $ induction base step sn0 where base :: Assoc (:*$$) (Zero nat) base = Assoc $ \ m l -> start (sZero %:* m %:* l) === sZero %:* l `because` multCongL (multZeroL m) l === sZero `because` multZeroL l === sZero %:* (m %:* l) `because` sym (multZeroL (m %:* l)) step :: Sing (n :: nat) -> Assoc (:*$$) n -> Assoc (:*$$) (S n) step n _ = Assoc $ \ m l -> start (sS n %:* m %:* l) === (n %:* m %:+ m) %:* l `because` multCongL (multSuccL n m) l === n %:* m %:* l %:+ m %:* l `because` plusMultDistrib (n %:* m) m l === n %:* (m %:* l) %:+ m %:* l `because` plusCongL (multAssoc n m l) (m %:* l) === sS n %:* (m %:* l) `because` sym (multSuccL n (m %:* l)) plusEqCancelL = plusEqCancelLProof . induction base step where base :: PlusEqCancelL (Zero nat) base = PlusEqCancelL $ \ l m nlnm -> start l === sZero %:+ l `because` sym (plusZeroL l) === sZero %:+ m `because` nlnm === m `because` plusZeroL m step :: Sing (n :: nat) -> PlusEqCancelL n -> PlusEqCancelL (Succ n) step n (PlusEqCancelL ih) = PlusEqCancelL $ \ l m snlsnm -> succInj $ ih (sS l) (sS m) $ start (n %:+ sS l) === sS (n %:+ l) `because` plusSuccR n l === sS n %:+ l `because` sym (plusSuccL n l) === sS n %:+ m `because` snlsnm === sS (n %:+ m) `because` plusSuccL n m === n %:+ sS m `because` sym (plusSuccR n m) plusEqCancelR n m l nlml = plusEqCancelL l n m $ start (l %:+ n) === (n %:+ l) `because` plusComm l n === (m %:+ l) `because` nlml === (l %:+ m) `because` plusComm m l succAndPlusOneL = proofSuccPlusL . induction base step where base :: SuccPlusL (Zero nat) base = SuccPlusL $ start (sSucc sZero) === sOne `because` succOneCong === sOne %:+ sZero `because` sym (plusZeroR sOne) step :: Sing (n :: nat) -> SuccPlusL n -> SuccPlusL (Succ n) step sn (SuccPlusL ih) = SuccPlusL $ start (sSucc (sSucc sn)) === sSucc (sOne %:+ sn) `because` succCong ih === sOne %:+ sSucc sn `because` sym (plusSuccR sOne sn) succAndPlusOneR n = start (sSucc n) === sOne %:+ n `because` succAndPlusOneL n === n %:+ sOne `because` plusComm sOne n zeroOrSucc = induction base step where base = IsZero step sn _ = IsSucc sn plusEqZeroL n m Refl = case zeroOrSucc n of { IsZero -> Refl IsSucc pn -> absurd $ succNonCyclic (pn %:+ m) (sym $ plusSuccL pn m) } plusEqZeroR n m = plusEqZeroL m n . trans (plusComm m n) predUnique n m snEm = start n === (sPred (sSucc n)) `because` sym (predSucc n) === sPred m `because` predCong snEm multEqSuccElimL n m l nmEsl = case zeroOrSucc n of { IsZero -> absurd $ succNonCyclic l $ sym $ start sZero === sZero %:* m `because` sym (multZeroL m) === sSucc l `because` nmEsl IsSucc pn -> succCong (predUnique pn n Refl) } multEqSuccElimR n m l nmEsl = multEqSuccElimL m n l (multComm m n `trans` nmEsl) minusZero n = start (n %:- sZero) === (n %:+ sZero) %:- sZero `because` minusCongL (sym $ plusZeroR n) sZero === n `because` plusMinus n sZero multEqCancelR = proofMultEqCancelR . induction base step where base :: MultEqCancelR (Zero nat) base = MultEqCancelR $ \ m l zslmsl -> sym $ plusEqZeroR (m %:* l) m $ sym $ start sZero === sZero %:* l `because` sym (multZeroL l) === sZero %:* l %:+ sZero `because` sym (plusZeroR (sZero %:* l)) === sZero %:* sSucc l `because` sym (multSuccR sZero l) === m %:* sSucc l `because` zslmsl === m %:* l %:+ m `because` multSuccR m l step :: Sing (n :: nat) -> MultEqCancelR n -> MultEqCancelR (Succ n) step n (MultEqCancelR ih) = MultEqCancelR $ \ m l snmssnl -> let m' = sPred m pf = start (m %:* sSucc l) === sSucc n %:* sSucc l `because` sym snmssnl === n %:* sSucc l %:+ sSucc l `because` multSuccL n (sSucc l) === sSucc (n %:* sSucc l %:+ l) `because` plusSuccR (n %:* sSucc l) l sm'Em = multEqSuccElimL m (sSucc l) (n %:* sSucc l %:+ l) pf pf' = ih m' l $ plusEqCancelR (n %:* sSucc l) (m' %:* sSucc l) (sSucc l) $ start (n %:* sSucc l %:+ sSucc l) === sSucc (n %:* sSucc l %:+ l) `because` plusSuccR (n %:* sSucc l) l === m %:* sSucc l `because` sym pf === sSucc m' %:* sSucc l `because` multCongL sm'Em (sSucc l) === (m' %:* sSucc l %:+ sSucc l) `because` multSuccL m' (sSucc l) in succCong pf' `trans` sym sm'Em succPred n nonZero = case zeroOrSucc n of { IsZero -> absurd $ nonZero Refl IsSucc n' -> sym $ succCong $ predUnique n' n Refl } multEqCancelL n m l snmEsnl = multEqCancelR m l n $ multComm m (sSucc n) `trans` snmEsnl `trans` multComm (sSucc n) l sPred' pxy sn = coerce (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn)

- Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_azZ6 :: Ordering). Sing t_azZ6 -> Sing (Apply FlipOrderingSym0 t_azZ6 :: Ordering)