proposition: Lemma FTA_a_la_Henk : forall f : CCX, {x : CC | {y : CC | AbsCC (f ! x[-]f ! y) [>][0]}} -> {z : CC | f ! z [=] [0]}.
proof: Proof. intros f H. elim H. intros x H0. elim H0. intros y H1. pose (H1':=(CAnd_proj1 _ _ (greater_def _ _ _) H1)). clearbody H1'. clear H1. rename H1' into H1. generalize (less_imp_ap _ _ _ H1); intro H2. generalize (AbsCC_ap_zero _ H2); intro H3. cut (Sum 0 (lth_of_poly f) (fun i : nat => nth_coeff i f[*] (x[^]i[-]y[^]i)) [#] [0]). intro H4. assert (0 <= lth_of_poly f) as H5 by auto with zarith. generalize (Sum_apzero _ _ _ _ H5 H4); intro H6. elim H6; intros i H8 H9. elim H8; intros H10 H11. apply FTA. unfold nonConst in |- *. generalize (cring_mult_ap_zero _ _ _ H9); intro H12. exists i. elim (zerop i). intro H13. exfalso. elim (ap_irreflexive_unfolded _ ([0]:CC)). rstepl (nth_coeff i f[*] (x[^]0[-]y[^]0)). rewrite <- H13. assumption. auto. assumption. apply ap_wdl_unfolded with (Sum 0 (lth_of_poly f) (fun i : nat => nth_coeff i f[*]x[^]i[-]nth_coeff i f[*]y[^]i)). 2: apply Sum_wd. 2: intro. 2: algebra. apply ap_wdl_unfolded with (Sum 0 (lth_of_poly f) (fun i : nat => nth_coeff i f[*]x[^]i) [-] Sum 0 (lth_of_poly f) (fun i : nat => nth_coeff i f[*]y[^]i)). 2: apply eq_symmetric_unfolded. 2: change (Sum 0 (lth_of_poly f) (fun j : nat => (fun i : nat => nth_coeff i f[*]x[^]i) j[-] (fun i : nat => nth_coeff i f[*]y[^]i) j) [=] Sum 0 (lth_of_poly f) (fun i : nat => nth_coeff i f[*]x[^]i) [-] Sum 0 (lth_of_poly f) (fun i : nat => nth_coeff i f[*]y[^]i)) in |- *. 2: apply Sum_minus_Sum. apply ap_wdl_unfolded with (f ! x[-]f ! y). 2: unfold cg_minus in |- *. 2: apply csbf_wd_unfolded. 2: apply poly_as_sum. 2: apply poly_degree_lth. 2: apply csf_wd_unfolded. 2: apply poly_as_sum. 2: apply poly_degree_lth. assumption. Qed.
imports: CoRN.fta.CPoly_Rev CoRN.fta.FTAreg