proposition: Theorem S_log_square_lt_h : forall y x, y = Nat.log2 x -> 6 <= Nat.log2 x-> S y * S y <= x.
proof: Proof. induction y; intuition; simpl in *. lia. assert (y = Nat.log2 (Nat.div2 x)). symmetry. eapply log2_div2. trivial. rewrite (Nat.mul_comm _ (S (S y))). simpl. rewrite (Nat.mul_comm _ (S y)) in IHy. simpl in *. assert ( S (S (y + S (S (y + (y + (y + y * y)))))) = (S (y + (y + y * y))) + (2 * y + 3)). lia. rewrite H2. clear H2. destruct (eq_nat_dec (Nat.log2 x) 6). assert (y = 5). assert (S y = 6). rewrite H. trivial. lia. rewrite H2. simpl. assert (x >= Nat.pow 2 6). rewrite <- e. eapply Nat.log2_spec. destruct (eq_nat_dec x 0). subst. rewrite log2_0 in H. lia. lia. eapply Nat.le_trans. 2:{ eapply H3. } simpl. lia. assert ( S (y + (y + y * y)) <= Nat.div2 x). eapply IHy. trivial. lia. assert (2 * y + 3 <= Nat.div2 x). eapply double_log_plus_3_le_h; trivial. lia. eapply Nat.le_trans. eapply Nat.add_le_mono. eapply H2. eapply H3. eapply div2_ge_double. Qed.
imports: FCF.StdNat FCF.Rat