proposition: Theorem S_log_square_lt : forall x, Nat.pow 2 6 <= x-> S (Nat.log2 x) * S (Nat.log2 x) <= x.
proof: Proof. intuition. eapply S_log_square_lt_h; trivial. eapply Nat.le_trans. 2:{ eapply Nat.log2_le_mono. eapply H. } rewrite Nat.log2_pow2; lia. Qed.
imports: FCF.StdNat FCF.Rat