proposition: Fact mult_lt_power_2_4' u1 v1 u2 v2 k : u1 < power k 2 -> v1 < power k 2 -> u2 < power k 2 -> v2 < power k 2 -> u1*v1+v2*u2 < power (4*k) 2.
proof: Proof. intros H1 H2 H3 H4. destruct (eq_nat_dec k 0) as [ ? | Hk ]. - subst k; simpl. rewrite power_0 in *. destruct u1; destruct v1; destruct u2; destruct v2; subst; lia. - apply Nat.lt_le_trans with (power (S (2*k)) 2). + rewrite power_S, <- mult_2_eq_plus. apply Nat.add_lt_mono; apply mult_lt_power_2; auto. + apply power_mono_l; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)