proposition: Theorem div_clean_dec2 : forall (d : nat) (a b : mon d), gb d (div_mon_clean d a b) = false -> mult_mon d (div_mon d a b) b <> a.
proof: Proof. intros d; elim d; simpl in |- *; auto. intros a H' H'0; inversion H'0; auto. intros n H' a b. case (le_lt_dec (pmon1 (S n) b) (pmon1 (S n) a)); simpl in |- *; auto. intros l; generalize (H' (pmon2 (S n) a) (pmon2 (S n) b)). case (div_mon_clean n (pmon2 (S n) a) (pmon2 (S n) b)); simpl in |- *; auto. intros H'0 b0 H'1 H'2; red in |- *; intros H'3. lapply H'1; [ intros H'4; apply H'4; clear H'1 | clear H'1 ]; auto. change (pmon2 (S n) (c_n n (pmon1 (S n) a - pmon1 (S n) b + pmon1 (S n) b) (mult_mon n (div_mon n (pmon2 (S n) a) (pmon2 (S n) b)) (pmon2 (S n) b))) = pmon2 (S n) a :>mon n) in |- *. rewrite H'3; auto. intros H'0 H'1; red in |- *; intros H'2; absurd (pmon1 (S n) a - pmon1 (S n) b + pmon1 (S n) b = pmon1 (S n) a); auto. 2: change (pmon1 (S n) (c_n n (pmon1 (S n) a - pmon1 (S n) b + pmon1 (S n) b) (mult_mon n (div_mon n (pmon2 (S n) a) (pmon2 (S n) b)) (pmon2 (S n) b))) = pmon1 (S n) a :>nat) in |- *. 2: rewrite H'2; auto. rewrite (minus_lt_0 (pmon1 (S n) b) (pmon1 (S n) a)); simpl in |- *; auto. red in |- *; intros H'3; absurd (pmon1 (S n) a < pmon1 (S n) b); auto. apply Nat.le_ngt; auto. rewrite H'3; auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)