proposition: Lemma mdiv_proj : forall (d : nat) (m m' : mon (S d)), pmon1 (S d) m <= pmon1 (S d) m' -> mdiv d (pmon2 (S d) m) (pmon2 (S d) m') -> mdiv (S d) m m'.
proof: Proof. intros d m m' H' H'0; rewrite <- (proj_ok d m); rewrite <- (proj_ok d m'); auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)