proposition: Lemma Ccpoly_double_comp_ind : forall P : cpoly_csetoid -> cpoly_csetoid -> CProp, (forall p1 p2 q1 q2, p1 [=] p2 -> q1 [=] q2 -> P p1 q1 -> P p2 q2) -> P cpoly_zero_cs cpoly_zero_cs -> (forall p q c d, P p q -> P (cpoly_linear_cs c p) (cpoly_linear_cs d q)) -> forall p q, P p q.
proof: Proof. intros. apply Ccpoly_double_ind0_cs. intro p0; pattern p0 in |- *; apply Ccpoly_ind_cs;[assumption|]. intros p1 c. intros. apply X with (cpoly_linear_cs c p1) (cpoly_linear_cs [0] cpoly_zero_cs). algebra. apply _cpoly_lin_eq_zero. split; algebra. apply X1; assumption. intro p0; pattern p0 in |- *; apply Ccpoly_ind_cs. assumption. intros. apply X with (cpoly_linear_cs [0] cpoly_zero_cs) (cpoly_linear_cs c p1). apply _cpoly_lin_eq_zero;split; algebra. algebra. apply X1; assumption. now apply X1. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational