proposition: Lemma Sumx_to_Sum : forall n, 0 < n -> forall f, nat_less_n_fun f -> Sumx f [=] Sum 0 (pred n) (part_tot_nat_fun G n f).
proof: Proof. intro n; induction n as [| n Hrecn]; intros H f Hf. exfalso; inversion H. cut (0 <= n); [ intro H0 | auto with arith ]. elim (le_lt_eq_dec _ _ H0); clear H H0; intro H. simpl in |- *. pattern n at 6 in |- *; rewrite <- (Nat.lt_succ_pred _ _ H). eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply Sum_last. apply bin_op_wd_unfolded. eapply eq_transitive_unfolded. apply Hrecn; auto. red in |- *; intros; apply Hf; auto. apply Sum_wd'. auto with arith. intros i H1 H2. cut (i < n); [ intro | lia ]. eapply eq_transitive_unfolded. apply part_tot_nat_fun_ch1 with (Hi := H0). red in |- *; intros; apply Hf; auto. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. apply part_tot_nat_fun_ch1 with (Hi := Nat.lt_lt_succ_r _ _ H0). red in |- *; intros; apply Hf; auto. algebra. rewrite -> (Nat.lt_succ_pred _ _ H). apply eq_symmetric_unfolded; apply part_tot_nat_fun_ch1; auto. generalize f Hf; clear Hf f; rewrite <- H. simpl in |- *; intros f Hf. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply Sum_one. astepl (f 0 (Nat.lt_succ_diag_r 0)). apply eq_symmetric_unfolded; apply part_tot_nat_fun_ch1; auto. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)