proposition: Lemma recomp_ok : forall (d : nat) (h : d <> 0) (m : mon d), recomp d h m = m.
proof: Proof. intros d h m. generalize h; clear h. elim m. intros h; elim h; auto. intros; simpl in |- *; unfold recomp in |- *; auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)