proposition: Fact convex_n_le n (f g : nat -> nat) : ∑ n (fun i => 2*(f i*g i)) <= ∑ n (fun i => f i*f i + g i*g i).
proof: Proof. revert f g; induction n as [ | n IHn ]; intros f g. + rewrite msum_0; auto. + do 2 rewrite msum_S. apply Nat.add_le_mono; auto. Qed.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)