proposition: Lemma linear_eq_zero_ : c[+X*]p [=] [0] -> c [=] [0] /\ p [=] [0].
proof: Proof. Proof cpoly_lin_eq_zero_ CR p c. Lemma _linear_eq_zero : c [=] [0] /\ p [=] [0] -> c[+X*]p [=] [0]. Proof _cpoly_lin_eq_zero CR p c. Lemma zero_eq_linear_ : [0] [=] c[+X*]p -> c [=] [0] /\ [0] [=] p. Proof cpoly_zero_eq_lin_ CR p c. Lemma _zero_eq_linear : c [=] [0] /\ [0] [=] p -> [0] [=] c[+X*]p. Proof _cpoly_zero_eq_lin CR p c. Lemma linear_eq_linear_ : c[+X*]p [=] d[+X*]q -> c [=] d /\ p [=] q. Proof cpoly_lin_eq_lin_ CR p q c d. Lemma _linear_eq_linear : c [=] d /\ p [=] q -> c[+X*]p [=] d[+X*]q. Proof _cpoly_lin_eq_lin CR p q c d. Lemma linear_ap_zero_ : c[+X*]p [#] [0] -> c [#] [0] or p [#] [0]. Proof cpoly_lin_ap_zero_ CR p c. Lemma _linear_ap_zero : c [#] [0] or p [#] [0] -> c[+X*]p [#] [0]. Proof _cpoly_lin_ap_zero CR p c. Lemma linear_ap_zero : (c[+X*]p [#] [0]) = (c [#] [0] or p [#] [0]). Proof cpoly_lin_ap_zero CR p c. Lemma zero_ap_linear_ : [0] [#] c[+X*]p -> c [#] [0] or [0] [#] p. Proof cpoly_zero_ap_lin_ CR p c. Lemma _zero_ap_linear : c [#] [0] or [0] [#] p -> [0] [#] c[+X*]p. Proof _cpoly_zero_ap_lin CR p c. Lemma zero_ap_linear : ([0] [#] c[+X*]p) = (c [#] [0] or [0] [#] p). Proof cpoly_zero_ap_lin CR p c. Lemma linear_ap_linear_ : c[+X*]p [#] d[+X*]q -> c [#] d or p [#] q. Proof cpoly_lin_ap_lin_ CR p q c d. Lemma _linear_ap_linear : c [#] d or p [#] q -> c[+X*]p [#] d[+X*]q. Proof _cpoly_lin_ap_lin CR p q c d. Lemma linear_ap_linear : (c[+X*]p [#] d[+X*]q) = (c [#] d or p [#] q). Proof cpoly_lin_ap_lin CR p q c d. End helpful_section. Lemma Ccpoly_induc : forall P : RX -> CProp, P [0] -> (forall p c, P p -> P (c[+X*]p)) -> forall p, P p. Proof (Ccpoly_ind_cs CR). Lemma Ccpoly_double_sym_ind : forall P : RX -> RX -> CProp, Csymmetric P -> (forall p, P p [0]) -> (forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q. Proof (Ccpoly_double_sym_ind0_cs CR). Lemma Cpoly_double_comp_ind : forall P : RX -> RX -> CProp, (forall p1 p2 q1 q2, p1 [=] p2 -> q1 [=] q2 -> P p1 q1 -> P p2 q2) -> P [0] [0] -> (forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q. Proof (Ccpoly_double_comp_ind CR). Lemma Cpoly_triple_comp_ind : forall P : RX -> RX -> RX -> CProp, (forall p1 p2 q1 q2 r1 r2, p1 [=] p2 -> q1 [=] q2 -> r1 [=] r2 -> P p1 q1 r1 -> P p2 q2 r2) -> P [0] [0] [0] -> (forall p q r c d e, P p q r -> P (c[+X*]p) (d[+X*]q) (e[+X*]r)) -> forall p q r, P p q r. Proof (Ccpoly_triple_comp_ind CR). Lemma cpoly_induc : forall P : RX -> Prop, P [0] -> (forall p c, P p -> P (c[+X*]p)) -> forall p, P p. Proof (cpoly_ind_cs CR). Lemma cpoly_double_sym_ind : forall P : RX -> RX -> Prop, Tsymmetric P -> (forall p, P p [0]) -> (forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q. Proof (cpoly_double_sym_ind0_cs CR). Lemma poly_double_comp_ind : forall P : RX -> RX -> Prop, (forall p1 p2 q1 q2, p1 [=] p2 -> q1 [=] q2 -> P p1 q1 -> P p2 q2) -> P [0] [0] -> (forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q. Proof (cpoly_double_comp_ind CR). Lemma poly_triple_comp_ind : forall P : RX -> RX -> RX -> Prop, (forall p1 p2 q1 q2 r1 r2, p1 [=] p2 -> q1 [=] q2 -> r1 [=] r2 -> P p1 q1 r1 -> P p2 q2 r2) -> P [0] [0] [0] -> (forall p q r c d e, P p q r -> P (c[+X*]p) (d[+X*]q) (e[+X*]r)) -> forall p q r, P p q r. Proof (cpoly_triple_comp_ind CR). Transparent cpoly_cring. Transparent cpoly_cgroup. Transparent cpoly_csetoid. Fixpoint cpoly_apply (p : RX) (x : CR) {struct p} : CR := match p with | cpoly_zero _ => [0] | cpoly_linear _ c p1 => c[+]x[*]cpoly_apply p1 x end. Lemma cpoly_apply_strext : bin_fun_strext _ _ _ cpoly_apply. Proof. unfold bin_fun_strext in |- *. do 2 intro. pattern x1, x2 in |- *. apply Ccpoly_double_sym_ind. unfold Csymmetric in |- *. intros. generalize (ap_symmetric _ _ _ X0); intro. elim (X _ _ X1); intro. left. apply ap_symmetric_unfolded. assumption. right. apply ap_symmetric_unfolded. assumption. do 3 intro. pattern p in |- *. apply Ccpoly_induc. simpl in |- *. intro H. elim (ap_irreflexive _ _ H). intros. simpl in X0. simpl in X. cut (c[+]y1[*]cpoly_apply p0 y1 [#] [0][+]y1[*][0]). intro. elim (cs_bin_op_strext _ _ _ _ _ _ X1); intro H2. left. cut (c [#] [0] or p0 [#] [0]). intro. apply _linear_ap_zero. auto. left. assumption. elim (cs_bin_op_strext _ _ _ _ _ _ H2); intro H3. elim (ap_irreflexive _ _ H3). elim (X H3); intro H4. left. cut (c [#] [0] or p0 [#] [0]). intro; apply _linear_ap_zero. auto. right. exact H4. auto. astepr ([0][+]([0]:CR)). astepr ([0]:CR). auto. simpl in |- *. intros. elim (cs_bin_op_strext _ _ _ _ _ _ X0); intro H1. auto. elim (cs_bin_op_strext _ _ _ _ _ _ H1); intro H2. auto. elim (X _ _ H2); auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational