proposition: Lemma mdiv_trans : forall d : nat, transitive (mon d) (mdiv d).
proof: Proof. intros d; elim d; unfold transitive in |- *; auto. - intros x y z mxy myz. apply mdiv_inv in mxy;apply mdiv_inv in myz. apply mdiv_inv. intuition. - intros n Rec x y z mxy myz. apply mdiv_inv in mxy;apply mdiv_inv in myz. destruct mxy as [vxy [vxy' [nxy [nxy' [Hnxy [Hdivxy [eq1 eq2]]]]]]]. destruct myz as [vyz [vyz' [nyz [nyz' [Hnyz [Hdivyz [eq3 eq4]]]]]]]. destruct eq1,eq2,eq4. injection eq3;clear eq3;intros eqv eqn. destruct eqn. pose proof (eq_sigT_snd eqv) as eqv'. rewrite (UIP_refl_nat n _) in eqv'. simpl in eqv';destruct eqv';clear eqv. apply mdiv_cons. * apply Nat.le_trans with (m := nyz); assumption. * apply Rec with (y := vyz); assumption. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)