proposition: Fact mult_lt_power_2 u v k : u < power k 2 -> v < power k 2 -> u*v < power (2*k) 2.
proof: Proof. intros H1 H2. replace (2*k) with (k+k) by lia. rewrite power_plus. apply Nat.lt_le_trans with ((S u)*S v). simpl; rewrite (Nat.mul_comm _ (S _)); simpl; rewrite Nat.mul_comm; lia. apply Nat.mul_le_mono; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)