proposition: Lemma prodcsetoid_is_CSetoid : forall A B : CSetoid, is_CSetoid (prodT A B) (prod_eq A B) (prod_ap A B).
proof: Proof. intros A B. apply (Build_is_CSetoid _ (prod_eq A B) (prod_ap A B)). intros x. case x. intros c c0 H. elim H. intros H1. now apply: (ap_irreflexive A _ H1). apply (ap_irreflexive B _ ). intros x y. case x. case y. intros c c0 c1 c2 H. elim H. intros. left. now apply ap_symmetric. intros. right. now apply ap_symmetric. intros x y. case x. case y. intros c c0 c1 c2 H z. case z. intros c3 c4. generalize H. intros. elim H. intros. cut (c1 [#] c3 or c3 [#] c). intros [H1|H2]. left. now left. intros. right. now left. now apply: ap_cotransitive. intros. cut (c2 [#] c4 or c4 [#] c0). intros [H1|H2]. left; now right. now right;right. now apply: ap_cotransitive. intros x y. case x. case y. intros c c0 c1 c2. split. intros. split. apply not_ap_imp_eq. intros H1. now cut (c1 [#] c or c2 [#] c0);[|left]. apply not_ap_imp_eq. intros H1. now cut (c1 [#] c or c2 [#] c0);[|right]. intros. elim H. intros H0 H1 H2. now elim H2;apply eq_imp_not_ap. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid