proposition: Theorem log_square_lt : forall x, Nat.pow 2 6 <= x-> Nat.log2 x * Nat.log2 x < x.
proof: Proof. intuition. assert (Nat.log2 x < S (Nat.log2 x)). lia. eapply Nat.lt_le_trans. eapply mult_lt_compat. eapply H0. eapply H0. eapply S_log_square_lt. trivial. Qed.
imports: FCF.StdNat FCF.Rat