proposition: Lemma cotransitive_cpoly_ap : cotransitive cpoly_ap.
proof: Proof. red in |- *. intros x y. pattern x, y in |- *. apply Ccpoly_double_sym_ind0. red in |- *; intros p q H H0 r. generalize (symmetric_cpoly_ap _ _ H0); intro H1. elim (H H1 r); intro H2; [ right | left ]; apply symmetric_cpoly_ap; assumption. simpl in |- *; intros p H z. generalize H. pattern p, z in |- *. apply Ccpoly_double_ind0'. simpl in |- *; intros q H0; elim H0. simpl in |- *; auto. simpl in |- *; intros r q c d H0 H1. elim H1; intro H2. generalize (ap_cotransitive_unfolded _ _ _ H2 d); intro H3. elim H3; auto. rewrite cpoly_ap_p_zero in H2. elim (H0 H2); auto. right; right; rewrite cpoly_ap_p_zero; assumption. intros p q c d H H0 r. simpl in H0. elim H0; intro H1. induction r as [| s r Hrecr]. simpl in |- *. generalize (ap_cotransitive_unfolded _ _ _ H1 [0]); intro H2. elim H2; auto. intro H3. right; left; apply ap_symmetric_unfolded; assumption. simpl in |- *. generalize (ap_cotransitive_unfolded _ _ _ H1 s); intro H2. elim H2; auto. induction r as [| s r Hrecr]. simpl in |- *. cut (cpoly_ap_zero p or cpoly_ap_zero q). intro H2; elim H2; auto. generalize H1; pattern p, q in |- *; apply Ccpoly_double_ind0. simpl in |- *. intros r H2. left; rewrite cpoly_ap_p_zero; assumption. auto. simpl in |- *. intros p0 q0 c0 d0 H2 H3. elim H3; intro H4. elim (ap_cotransitive_unfolded _ _ _ H4 [0]); intro H5. auto. right; left; apply ap_symmetric_unfolded; assumption. elim (H2 H4); auto. simpl in |- *. elim (H H1 r); auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational