proposition: Theorem ppcm_mom_is_ppcm : forall (d : nat) (a b c : mon d), c = mult_mon d (div_mon d c a) a -> c = mult_mon d (div_mon d c b) b -> c = mult_mon d (div_mon d c (ppcm_mon d a b)) (ppcm_mon d a b).
proof: Proof. intros d; elim d; simpl in |- *; auto. intros n H' a b c H'0 H'1. rewrite <- (H' (pmon2 (S n) a) (pmon2 (S n) b) (pmon2 (S n) c)); auto. 2: change (pmon2 (S n) c = pmon2 (S n) (c_n n (pmon1 (S n) c - pmon1 (S n) a + pmon1 (S n) a) (mult_mon n (div_mon n (pmon2 (S n) c) (pmon2 (S n) a)) (pmon2 (S n) a))) :>mon n) in |- *; auto. 2: rewrite <- H'0; auto. 2: change (pmon2 (S n) c = pmon2 (S n) (c_n n (pmon1 (S n) c - pmon1 (S n) b + pmon1 (S n) b) (mult_mon n (div_mon n (pmon2 (S n) c) (pmon2 (S n) b)) (pmon2 (S n) b))) :>mon n) in |- *; auto. 2: rewrite <- H'1; auto. rewrite Nat.sub_add; auto. rewrite <- (proj_ok n c); auto. apply Nat.max_case; auto. apply plus_minus_le; auto. change (pmon1 (S n) (c_n n (pmon1 (S n) c - pmon1 (S n) a + pmon1 (S n) a) (mult_mon n (div_mon n (pmon2 (S n) c) (pmon2 (S n) a)) (pmon2 (S n) a))) = pmon1 (S n) c :>nat) in |- *; auto. rewrite <- H'0; auto. apply plus_minus_le; auto. change (pmon1 (S n) (c_n n (pmon1 (S n) c - pmon1 (S n) b + pmon1 (S n) b) (mult_mon n (div_mon n (pmon2 (S n) c) (pmon2 (S n) b)) (pmon2 (S n) b))) = pmon1 (S n) c :>nat) in |- *; auto. rewrite <- H'1; auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)