proposition: Lemma partitionOfUnity : forall n, @Sumx (cpoly_cring R) _ (fun i H => Bernstein (proj1 (Nat.lt_succ_r i n) H)) [=][1].
proof: Proof. induction n. reflexivity. set (A:=(fun (i : nat) (H : i < S n) => Bernstein (proj1 (Nat.lt_succ_r i n) H))) in *. set (B:=(fun i => ([1][-]_X_)[*](part_tot_nat_fun (cpoly_cring R) _ A i)[+]_X_[*]match i with O => [0] | S i' => (part_tot_nat_fun _ _ A i') end)). rewrite -> (fun a b => Sumx_Sum0 _ a b B). unfold B. rewrite -> Sum0_plus_Sum0. do 2 rewrite -> mult_distr_sum0_lft. rewrite -> Sumx_to_Sum in IHn; auto with *. setoid_replace (Sum0 (S (S n)) (part_tot_nat_fun (cpoly_cring R) (S n) A)) with (Sum0 (S (S n)) (part_tot_nat_fun (cpoly_cring R) (S n) A)[-][0]) using relation (@st_eq (cpoly_cring R)) by ring. change (Sum0 (S (S n)) (part_tot_nat_fun (cpoly_cring R) (S n) A)[-][0]) with (Sum 0 (S n) (part_tot_nat_fun (cpoly_cring R) (S n) A)). set (C:=(fun i : nat => match i with | 0 => ([0] : cpoly_cring R) | S i' => part_tot_nat_fun (cpoly_cring R) (S n) A i' end)). setoid_replace (Sum0 (S (S n)) C) with (Sum0 (S (S n)) C[-][0]) using relation (@st_eq (cpoly_cring R)) by ring. change (Sum0 (S (S n)) C[-][0]) with (Sum 0 (S n) C). rewrite -> Sum_last. rewrite -> IHn. replace (part_tot_nat_fun (cpoly_cring R) (S n) A (S n)) with ([0]:cpoly_cring R). rewrite -> Sum_first. change (C 0) with ([0]:cpoly_cring R). rewrite <- (Sum_shift _ (part_tot_nat_fun (cpoly_cring R) (S n) A)) by reflexivity. rewrite -> IHn by ring. ring. unfold part_tot_nat_fun. destruct (le_lt_dec (S n) (S n)). reflexivity. exfalso; lia. intros i j Hij. subst. intros Hi Hj. unfold A. replace (proj1 (Nat.lt_succ_r j n) Hi) with (proj1 (Nat.lt_succ_r j n) Hj) by apply le_irrelevent. apply eq_reflexive. destruct i; intros Hi; unfold B, A, part_tot_nat_fun. simpl. symmetry. rewrite <- (le_irrelevent _ _ (Nat.le_0_l _) _). ring. destruct (le_lt_dec (S n) i). exfalso; lia. destruct (le_lt_dec (S n) (S i)); simpl (Bernstein (proj1 (Nat.lt_succ_r (S i) (S n)) Hi)); destruct (le_lt_eq_dec (S i) (S n) (proj1 (Nat.lt_succ_r (S i) (S n)) Hi)). exfalso; lia. replace (proj1 (Nat.lt_succ_r i n) (proj1 (Nat.lt_succ_r (S i) (S n)) Hi)) with (proj1 (Nat.lt_succ_r i n) l) by apply le_irrelevent. ring. replace (le_S_n i n (proj1 (Nat.lt_succ_r (S i) (S n)) Hi)) with (proj1 (Nat.lt_succ_r i n) l) by apply le_irrelevent. replace l1 with l0 by apply le_irrelevent. reflexivity. exfalso; lia. Qed.
imports: CoRN.algebra.CPolynomials CoRN.algebra.CSums CoRN.tactics.Rational CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.algebra.CRing_Homomorphisms Coq(Lia)