proposition: Fact convex_n_eq n (f g : nat -> nat) : ∑ n (fun i => 2*(f i*g i)) = ∑ n (fun i => f i*f i + g i*g i) <-> forall i, i < n -> f i = g i.
proof: Proof. split. + revert f g; induction n as [ | n IHn ]; intros f g. * intros; lia. * do 2 rewrite msum_S; intros H. apply nat_le_sum in H; auto. destruct H as (H1 & H2). apply convex_eq in H1. specialize (IHn _ _ H2). intros [ | ] ?; auto; apply IHn; lia. + intros Hfg. apply msum_ext. intros i Hi; rewrite Hfg; auto; ring. Qed.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)