proposition: Fact const_u_square : u * u = u1 + u2.
proof: Proof. Proof using Hl Hlq Hw Hu Hm. unfold u1, u2. rewrite Hu, square_sum; f_equal. + apply msum_ext; intros; rewrite <- power_plus; f_equal; lia. + rewrite <- sum_0n_scal_l; apply msum_ext; intros i Hi. rewrite <- sum_0n_scal_l; apply msum_ext; intros j Hj. rewrite power_plus; ring. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)