proposition: Lemma cpoly_double_ind0 : forall P : cpoly -> cpoly -> Prop, (forall p, P p cpoly_zero) -> (forall p, P cpoly_zero p) -> (forall p q c d, P p q -> P (cpoly_linear c p) (cpoly_linear d q)) -> forall p q, P p q.
proof: Proof. simple induction p; auto. simple induction q; auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational