proposition: Lemma Sumx_resp_less : forall n, 0 < n -> forall f g : forall i, i < n -> R, (forall i H, f i H [<] g i H) -> Sumx f [<] Sumx g.
proof: Proof. simple induction n. intros; simpl in |- *; exfalso; inversion H. simple induction n0. intros. clear H. simpl in |- *; apply plus_resp_less_lft. apply X0. intros. simpl in |- *. apply plus_resp_less_both. astepl (Sumx (fun (i : nat) (l : i < S n1) => f i (Nat.lt_lt_succ_r _ _ l))). astepr (Sumx (fun (i : nat) (l : i < S n1) => g i (Nat.lt_lt_succ_r _ _ l))). apply X0. auto with arith. intros. apply X1. apply X1. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)