proposition: Lemma positive_Sumx : forall n (f : forall i, i < n -> R), nat_less_n_fun f -> [0] [<] Sumx f -> {i : nat | {H : i < n | [0] [<] f i H}}.
proof: Proof. simple induction n. simpl in |- *. intros; exfalso; generalize X; apply less_irreflexive_unfolded. simple induction n0. simpl in |- *. intros. exists 0. exists (Nat.lt_succ_diag_r 0). eapply less_wdr. apply X0. astepl (f _ (Nat.lt_succ_diag_r 0)). apply H; auto. simpl in |- *; intros. clear X. cut ([0] [<] f _ (Nat.lt_succ_diag_r (S n1)) or [0] [<] Sumx (fun (i : nat) (l : i < n1) => f i (Nat.lt_lt_succ_r i (S n1) (Nat.lt_lt_succ_r i n1 l)))[+] f n1 (Nat.lt_lt_succ_r n1 (S n1) (Nat.lt_succ_diag_r n1))). intro X. inversion_clear X. exists (S n1). exists (Nat.lt_succ_diag_r (S n1)). eapply less_wdr. apply X2. apply H; auto. set (f' := fun (i : nat) (H : i < S n1) => f i (Nat.lt_lt_succ_r _ _ H)) in *. cut {i : nat | {H : i < S n1 | [0] [<] f' i H}}; intros. elim X; intros i Hi; elim Hi; clear X2 Hi; intros Hi Hi'. exists i. exists (Nat.lt_lt_succ_r _ _ Hi). eapply less_wdr. apply Hi'. unfold f' in |- *; simpl in |- *. apply H; auto. apply X0. red in |- *. intros i j Hij. rewrite Hij. unfold f' in |- *. intros H0 H'. apply H; auto. apply X2; assumption. apply positive_Sum_two. eapply less_wdr. 2: apply cag_commutes_unfolded. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)