proposition: Theorem ppcm_prop_l : forall (d : nat) (a b : mon d), ppcm_mon d a b = mult_mon d (div_mon d (ppcm_mon d a b) a) a.
proof: Proof. intros d; elim d; simpl in |- *; auto. intros n H' a b; pattern (ppcm_mon n (pmon2 (S n) a) (pmon2 (S n) b)) at 1 in |- *; rewrite (H' (pmon2 (S n) a) (pmon2 (S n) b)). pattern (Nat.max (pmon1 (S n) a) (pmon1 (S n) b)) at 1 in |- *; rewrite Nat.sub_add; auto. apply Nat.le_max_l; auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)