proposition: Lemma cpoly_double_ind : forall P : Cpoly_cring -> Cpoly_cring -> Prop, (forall p, P p [0]) -> (forall p, P [0] p) -> (forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
proof: Proof. Proof (cpoly_double_ind0_cs CR). End Poly_Prop_Induction. #[global] Hint Resolve poly_linear cpoly_lin: algebra. #[global] Hint Resolve apply_wd cpoly_const_eq: algebra_c. #[global] Hint Resolve c_apply x_apply inv_apply plus_apply minus_apply mult_apply nexp_apply: algebra. #[global] Hint Resolve one_apply c_zero c_one c_mult: algebra. #[global] Hint Resolve poly_inv_apply: algebra. #[global] Hint Resolve c_mult_lin: algebra. #[global] Hint Rewrite one_apply c_apply x_apply mult_apply plus_apply minus_apply : apply. #[global] Hint Rewrite inv_apply nexp_apply c_mult_apply poly_inv_apply : apply. Ltac poly_apply:= autorewrite with apply; simpl. Section Derivative. Variable R:CRing. Add Ring cpolycring_thR1 : (cpoly_ring_th R). Notation RX:= (cpoly_cring R). Fixpoint cpoly_diff (p : RX) : RX := match p with | cpoly_zero _ => [0] | cpoly_linear _ c p1 => p1[+]([0][+X*](cpoly_diff p1)) end. Lemma cpoly_diff_strext : un_op_strext _ cpoly_diff. Proof. intros x. induction x. induction y. auto with *. intros Hxy. right. abstract ( destruct (cpoly_ap_zero_plus _ _ _ (ap_symmetric _ _ _ Hxy)) as [c|[c|c]]; [apply (ap_symmetric _ _ _ c) |elim (ap_irreflexive _ _ c) |apply IHy;apply c]). intros [|a y] Hxy. simpl in Hxy. right. abstract ( destruct (cpoly_ap_zero_plus _ _ _ Hxy) as [c|[c|c]]; [apply (ap_symmetric _ _ _ c) |elim (ap_irreflexive _ _ c) |change ([0][#]x); apply ap_symmetric; apply IHx; apply ap_symmetric; apply c]). right. destruct (cpoly_plus_op_strext _ _ _ _ _ Hxy) as [c|[c|c]]. assumption. elim (ap_irreflexive _ _ c). apply IHx; apply c. Defined.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational