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