proposition: Fact convex_le x y : 2*(x*y) <= x*x+y*y.
proof: Proof. destruct (le_lt_dec x y). + replace y with (x+(y-x)) by lia. apply convex_1. + rewrite (Nat.mul_comm x y), Nat.add_comm. replace x with (y+(x-y)) by lia. apply convex_1. Qed.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)