--#include "alfa/Nat.alfa"

package NatProofs where
  open Logic  use  subst,  substSym,  sym,  trans,  cong,  (===)
  open Module_Prelude  use  (==),  PredTrue
  open Module_Nat
   use  Nat,  cmpNat,  plus,  len,  index,  derived__Nat_Eq_Nat,  eqNat,
        NatEq,  CongSucc,  EqNatRefl,  oLt,  ltNat,  NotLtZero,
        AddSucc,  AddZero,  Peano4,  Peano4b,  oLe,  leNat,  LeNatRefl,
        LtNatSucc,  LeNatSucc,  LtNatPlus,  PredO,  PredS,
        inst__Nat_5_1,  derived__Nat_Show_Nat,  inst__Nat_12_1
  congSucc (a::Nat)(b::Nat)(p::(===) Nat a b)
    :: (===) Nat (S@_ a) (S@_ b)
    = cong Nat Nat a b (\(h::Nat) -> S@_ h) p
  eqId (a::Nat)(b::Nat)(p::PredTrue (eqNat a b)) :: (===) Nat a b
    = case a of {
        (O) ->
          case b of {
            (O) -> Ref@_;
            (S x1) -> case p of { };};
        (S x1) ->
          case b of {
            (O) -> case p of { };
            (S x1') -> congSucc x1 x1' (eqId x1 x1' p);};}
  eqNatRefl (a::Nat) :: PredTrue (eqNat a a)
    = case a of {
        (O) -> TrivialityIntro;
        (S x1) -> eqNatRefl x1;}
  idEq (a::Nat)(b::Nat)(p::(===) Nat a b) :: PredTrue (eqNat a b)
    = subst Nat a b (\(h::Nat) -> PredTrue (eqNat a h)) p (eqNatRefl a)
  proofNatEq :: NatEq
    = \(a::Nat) ->
      \(b::Nat) ->
      AndIntro
        (Implies (PredTrue (eqNat a b)) ((===) Nat a b))
        (Implies ((===) Nat a b) (PredTrue (eqNat a b)))
        (ImpliesIntro (PredTrue (eqNat a b)) ((===) Nat a b) (eqId a b))
        (ImpliesIntro ((===) Nat a b) (PredTrue (eqNat a b)) (idEq a b))
  proofCongSucc :: CongSucc
    = \(a::Nat) ->
      \(b::Nat) ->
      ImpliesIntro
        (Logic.(===) Nat a b)
        (Logic.(===) Nat (S@_ a) (S@_ b))
        (congSucc a b)
  proofEqNatRefl :: EqNatRefl
    = eqNatRefl
  proofNotLtZero :: NotLtZero
    = \(a::Nat) ->
      case a of {
        (O) -> TrivialityIntro;
        (S x1) -> TrivialityIntro;}
  addSucc (a::Nat)(b::Nat)
    :: (===) Nat (S@_ (plus a b)) (plus a (S@_ b))
    = case a of {
        (O) -> Ref@_;
        (S x1) -> congSucc (plus (S@_ x1) b) (plus x1 (S@_ b)) (addSucc x1 b);}
  proofAddSucc :: AddSucc
    = addSucc
  succCong (a::Nat)(b::Nat)(p::(===) Nat (S@_ a) (S@_ b))
    :: (===) Nat a b
    = eqId a b (idEq (S@_ a) (S@_ b) p)
  peano4 (n::Nat) :: (===) Nat (S@_ n) O@_ -> Absurdity
    = idEq (S@_ n) O@_
  peano4n (n::Nat) :: (===) Nat (S@_ n) n -> Absurdity
    = case n of {
        (O) -> peano4 O@_;
        (S x1) ->
          \(h::(===) Nat (S@_ (S@_ x1)) (S@_ x1)) ->
          peano4n x1 (succCong (S@_ x1) x1 h);}
  peano4' (n::Nat)(m::Nat) :: (===) Nat (plus m (S@_ n)) n -> Absurdity
    = case m of {
        (O) -> peano4n n;
        (S x1) ->
          case n of {
            (O) -> peano4 (plus x1 (S@_ O@_));
            (S x1') ->
              \(h::(===) Nat (plus (S@_ x1) (S@_ (S@_ x1'))) (S@_ x1')) ->
              peano4'
                x1'
                (S@_ x1)
                (succCong
                   (plus (S@_ x1) (S@_ x1'))
                   x1'
                   (trans
                      Nat
                      (S@_ (plus (S@_ x1) (S@_ x1')))
                      (plus (S@_ x1) (S@_ (S@_ x1')))
                      (S@_ x1')
                      (addSucc (S@_ x1) (S@_ x1'))
                      h));};}
  peano4b (a::Nat)(b::Nat)
    :: (p::(===) Nat (plus (S@_ a) b) b) -> Absurdity
    = substSym
        Nat
        (plus (S@_ a) b)
        (plus a (S@_ b))
        (\(h::Nat) -> (===) Nat h b -> Absurdity)
        (addSucc a b)
        (peano4' b a)
  proofPeano4 :: Peano4
    = \(a::Nat) ->
      ImpliesIntro
        (Logic.(===) Nat (S@_ a) O@_)
        Propositions.Absurdity
        (\(hyp::Logic.(===) Nat (S@_ a) O@_) -> peano4 a hyp)
  proofPeano4b :: Peano4b
    = \(a::Nat) ->
      \(b::Nat) ->
      ImpliesIntro
        ((===) Nat (S@_ (plus a b)) b)
        Absurdity
        (\(hyp::(===) Nat (S@_ (plus a b)) b) -> peano4b a b hyp)
  proofAddZero :: AddZero
    = \(a::Nat) ->
      case a of {
        (O) -> Ref@_;
        (S x1) -> congSucc x1 (plus x1 O@_) (proofAddZero x1);}
  natLeRefl (n::Nat) :: PredTrue (leNat n n)
    = case n of {
        (O) -> TrivialityIntro;
        (S x1) -> natLeRefl x1;}
  natLtSucc (a::Nat)(b::Nat) :: PredTrue (ltNat a (plus (S@_ b) a))
    = case a of {
        (O) -> TrivialityIntro;
        (S x1) ->
          subst
            Nat
            (S@_ (plus (S@_ b) x1))
            (plus (S@_ b) (S@_ x1))
            (\(h::Nat) -> PredTrue (ltNat (S@_ x1) h))
            (addSucc (S@_ b) x1)
            (natLtSucc x1 b);}
  natLeSucc (a::Nat)(b::Nat) :: PredTrue (leNat a (plus (S@_ b) a))
    = case a of {
        (O) -> TrivialityIntro;
        (S x1) ->
          subst
            Nat
            (S@_ (plus (S@_ b) x1))
            (plus (S@_ b) (S@_ x1))
            (\(h::Nat) -> PredTrue (leNat a h))
            (addSucc (S@_ b) x1)
            (natLeSucc x1 b);}
  natLtPlus (a::Nat)(b::Nat)(c::Nat)(p::PredTrue (ltNat a b))
    :: PredTrue (ltNat (plus a c) (plus b c))
    = case c of {
        (O) ->
          subst
            Nat
            a
            (plus a O@_)
            (\(h::Nat) -> PredTrue (ltNat h (plus b O@_)))
            (proofAddZero a)
            (subst
               Nat
               b
               (plus b O@_)
               (\(h::Nat) -> PredTrue (ltNat a h))
               (proofAddZero b)
               p);
        (S x1) ->
          subst
            Nat
            (S@_ (plus a x1))
            (plus a (S@_ x1))
            (\(h::Nat) -> PredTrue (ltNat h (plus b (S@_ x1))))
            (addSucc a x1)
            (subst
               Nat
               (S@_ (plus b x1))
               (plus b (S@_ x1))
               (\(h::Nat) -> PredTrue (ltNat (S@_ (plus a x1)) h))
               (addSucc b x1)
               (natLtPlus a b x1 p));}
  natPlusLt (a::Nat)
            (b::Nat)
            (c::Nat)
            (p::PredTrue (ltNat (plus a c) (plus b c)))
    :: PredTrue (ltNat a b)
    = case c of {
        (O) ->
          substSym
            Nat
            b
            (plus b O@_)
            (\(h::Nat) -> PredTrue (ltNat a h))
            (proofAddZero b)
            (substSym
               Nat
               a
               (plus a O@_)
               (\(h::Nat) -> PredTrue (ltNat h (plus b O@_)))
               (proofAddZero a)
               p);
        (S x1) ->
          natPlusLt
            a
            b
            x1
            (substSym
               Nat
               (S@_ (plus b x1))
               (plus b (S@_ x1))
               (\(h::Nat) -> PredTrue (ltNat (S@_ (plus a x1)) h))
               (addSucc b x1)
               (substSym
                  Nat
                  (S@_ (plus a x1))
                  (plus a (S@_ x1))
                  (\(h::Nat) -> PredTrue (ltNat h (plus b (S@_ x1))))
                  (addSucc a x1)
                  p));}
  proofLeNatRefl :: LeNatRefl
    = natLeRefl
  proofLtNatSucc :: LtNatSucc
    = natLtSucc
  proofLeNatSucc :: LeNatSucc
    = natLeSucc
  proofLtNatPlus :: LtNatPlus
    = \(a::Nat) ->
      \(b::Nat) ->
      \(c::Nat) ->
      ImpliesIntro
        (Module_Prelude.PredTrue (oLt (cmpNat a b)))
        (Module_Prelude.PredTrue (oLt (cmpNat (plus a c) (plus b c))))
        (natLtPlus a b c)
{-# Alfa unfoldgoals off
brief on
hidetypeannots on
wide

nd
hiding on
var "congSucc" hide 2
var "eqId"
var "succCong" hide 2
 #-}