The Coq mailing list

[Jean-Marc Notin <notin AT lix.polytechnique.fr>]

And now the proofs of the last two theorems... I tried not to use
automatic tactics, so the proofs may seem more complicated than those
from the standard library.

Theorem comm_mult : forall a b : nat, mult a b = mult b a.
Proof.
  induction a; simpl; intro b.
    rewrite multO; trivial.
    
    replace (S a) with (sum a (S O)).
    rewrite distrib_mult_sum.
    rewrite commute_sum. rewrite IHa. 
    repeat rewrite mult1; trivial.
    
    rewrite commute_sum; trivial.
Qed.

Theorem trans_mult : forall a b c : nat, mult a (mult b c) = mult (mult
a b) c.
Proof.
  induction a; simpl.
    trivial.

    intros b c.
    rewrite IHa.
    replace (sum (mult b c) (mult (mult a b) c)) with (sum (mult c b)
(mult c (mult a b))).
    rewrite <- distrib_mult_sum. apply comm_mult; trivial.
    
    rewrite (comm_mult  (mult a b) c); rewrite (comm_mult c b); trivial.
Qed.

-- 
Jean-Marc Notin
LIX - Équipe LogiCal

Attachment: signature.asc
Description: Ceci est une partie de message numériquement signée