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