proposition: Theorem div_clean_dec1 : forall (d : nat) (a b : mon d), gb d (div_mon_clean d a b) = true -> gm d (div_mon_clean d a b) = div_mon d a b /\ mult_mon d (div_mon d a b) b = a.
proof: Proof. intros d; elim d; simpl in |- *; auto. intros n H' a b; case (le_lt_dec (pmon1 (S n) b) (pmon1 (S n) a)); simpl in |- *; auto. 2: intros H'0 H'1; inversion H'1. 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 m b' H1 H2. case (H1 H2); intros H3 H4; split; auto. rewrite H3; auto. rewrite Nat.sub_add; auto. rewrite H4; auto. exact (proj_ok n a). Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)