proposition: Lemma lognat_correct1 : forall(b a : nat)(pf : a <> 0), (lognat pf) = b -> (expnat 2 b) <= a.
proof: Proof. induction b. intros. simpl in *. lia. intros. elim (nat_comp a). intros. destruct H0. subst. destruct (eq_nat_dec x 0). subst. lia. rewrite <- (lognat_prod_sum n pf) in H. inversion H. clear H. rewrite H1. apply IHb in H1. simpl in *. lia. subst. destruct (eq_nat_dec x 0). subst. unfold lognat in H. simpl in *. lia. assert ((2 * x) <> 0). lia. rewrite (lognat_odd x H0 pf) in H. rewrite <- (lognat_prod_sum n H0) in H. inversion H. rewrite H2. apply IHb in H2. simpl. lia. Qed.
imports: ZArith micromega.Lia