proposition: Lemma mdiv_inv : forall d x y, mdiv d x y <-> match d return mon d -> mon d -> Prop with | 0 => fun x y => n_0 = x /\ n_0 = y | S d => fun x y => exists v v' n n', n <= n' /\ mdiv d v v' /\ c_n d n v = x /\ c_n d n' v' = y end x y.
proof: Proof. intros d x y;split. - intros m;destruct m;eauto 8. - destruct d;intros m. + destruct m as [[] []];constructor. + destruct m as [? [? [? [? [? [? [[] []]]]]]]]. constructor;assumption. Defined.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)