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