proposition: Lemma cpoly_double_ind0_cs : forall P : cpoly_csetoid -> cpoly_csetoid -> Prop, (forall p, P p cpoly_zero_cs) -> (forall p, P cpoly_zero_cs p) -> (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. simple induction p. auto. simple induction q. auto. simpl in H1. unfold cpoly_linear_cs in H1. auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational