Given:

    data Nat = Zero | Succ Nat
    
    plus Zero m = m
    plus (Succ n) m = Succ (plus n m)
    
    mult Zero m = Zero
    mult (Succ n) m = plus n (mult n m)
    
Prove:

    for all x :: Nat, y::Nat . plus x y = plus y x
    
    Proof by induction, on x :: Nat:
    
        Base case: x = Zero
        
[ goal is now ]     plus Zero y = plus y Zero       { goal propn with x = Zero }

                    y = plus y Zero                 { LHS, by first eqn for plus }
                    
                    y = y                           { Lemma 1: for all n, plus n Zero = n }
                    
        Recursive case: x = Succ z
        
        Therefore, assuming:    for all y. plus z y = plus y z
        
                plus (Succ z) y = plus y (Succ z)   { goal propn with x = Succ z }
                    
                Succ (plus z y) = plus y (Succ z)   { LHS, by snd. eqn for plus }
                    
                Succ (plus y z) = plus y (Succ z)   { LHS, by ind. assm. }
                
                Succ (plus y z) = Succ (plus y z)   { RHS, Lemma 2: plus y (Succ z) = Succ (plus y z) }

                QED

Lemma 1:

    Prove for all n :: Nat, plus n Zero = n
                    
        Proof by induction on n :: Nat.
        
            Base case: n = Zero:
            
                plus Zero Zero = Zero                   { goal propn with n = Zero }
                
                Zero = Zero                             { LHS by fst rules plus }
                
                QED / trivial, since LHS = RHS / etc.
                
            Recursive case: n = Succ q
            Assume plus q Zero = q.
            
[ local ind. goal ]     plus (Succ q) Zero = Succ q

                        Succ (plus q Zero) = Succ q     { LHS by snd rule plus }
                        
                        Succ q = Succ q                 { by ind. assm. }
                        
                        QED

Lemma 2

        for all y :: Nat, z :: Nat. plus y (Succ z) = Succ (plus y z)
        
        Proof by induction on y:
        
        Base case: y = Zero
        
                plus Zero (Succ z) = Succ (plus Zero z)         { sub-goal with y = Zero }
                
                Succ z = Succ (plus Zero z)                     { LHS, by fst rule plus }
                
                Succ z = Succ z                                 { RHS, by fst rule plus }
                
                QED
                
        Recursive case: 
        
        Assume:     plus w (Succ z) = Succ (plus w z)
        
        Prove:      plus (Succ w) (Succ z) = Succ (plus (Succ w) z)
        
                    Succ (plus w (Succ z)) = Succ (plus (Succ w) z) { LHS, by snd rule plus }
                    
                    Succ (Succ (plus w z)) = Succ (plus (Succ w) z) { LHS, by ind. assm. }
                    
                    Succ (Succ (plus w z)) = Succ (Succ (plus w z)) { RHS, by snd rule plus }
                    
                    QED