proposition: Lemma negative_Sumx : forall n (f : forall i, i < n -> R), nat_less_n_fun f -> Sumx f [<] [0] -> {i : nat | {H : i < n | f i H [<] [0]}}.
proof: Proof. intros. cut {i : nat | {H : i < n | [0] [<] [--](f i H)}}. intro H1. elim H1; intros i Hi; elim Hi; clear X Hi; intros Hi Hi'. exists i; exists Hi. astepl ([--][--](f i Hi)); astepr ([--]([0]:R)); apply inv_resp_less; assumption. apply positive_Sumx with (f := fun (i : nat) (H : i < n) => [--](f i H)). red in |- *; intros. apply un_op_wd_unfolded; apply H; assumption. astepl ([--]([0]:R)); apply less_wdr with ([--](Sumx f)). apply inv_resp_less; assumption. generalize f H; clear X H f. induction n as [| n Hrecn]. simpl in |- *. intros; algebra. intros. simpl in |- *. rstepl ([--](Sumx (fun (i : nat) (l : i < n) => f i (Nat.lt_lt_succ_r i n l)))[+] [--](f n (Nat.lt_succ_diag_r n))). apply bin_op_wd_unfolded. 2: algebra. apply Hrecn with (f := fun (i : nat) (l : i < n) => f i (Nat.lt_lt_succ_r i n l)). red in |- *; intros; apply H; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)