proposition: Lemma irreflexive_cpoly_ap : irreflexive cpoly_ap.
proof: Proof. red in |- *. intro p; induction p as [| s p Hrecp]. intro H; elim H. intro H. elim H. apply ap_irreflexive_unfolded. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational