proposition: Lemma proj_ok : forall (d : nat) (m : mon (S d)), c_n d (pmon1 (S d) m) (pmon2 (S d) m) = m.
proof: Proof. intros d m; cut (S d <> 0); auto. intros H; cut (recomp (S d) H m = m); auto. apply recomp_ok; auto. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)