proposition: Lemma lognat_prod_sum_gen_h : forall (a' a b: nat)(pf1 : (a <> 0))(pf2 : (b <> 0))(pf3 : a * b <> 0), lognat pf1 = a' -> a' + lognat pf2 <= lognat pf3.
proof: Proof. induction a'; intros. simpl. eapply lognat_monotonic. induction a. congruence. simpl. intuition. destruct (nat_comp a). destruct H0. subst. assert (x <> 0). lia. assert (x * b <> 0). destruct x; destruct b; simpl; congruence. rewrite <- (lognat_prod_sum H0) in H. assert (lognat pf3 = S (lognat H1)). generalize pf3. rewrite <-Nat.mul_assoc. intros. rewrite (lognat_prod_sum _ pf0). trivial. rewrite H2. inversion H. specialize (IHa' x b H0 pf2 H1 H4). subst. lia. destruct (eq_nat_dec x 0). subst. unfold lognat in *. simpl in *. discriminate. assert (2 * x <> 0). lia. assert (x * b <> 0). destruct x; destruct b; simpl; congruence. assert (2 * x * b <> 0). rewrite <-Nat.mul_assoc. lia. subst. rewrite (lognat_odd _ H1) in H. rewrite <- (lognat_prod_sum n) in H. inversion H. subst. assert (lognat n = lognat n). trivial. specialize (IHa' x b n pf2 H2 H0). generalize pf3. assert (S (2 * x) * b = b + 2 * x * b). intuition. rewrite H4. intros. eapply Nat.le_trans. 2:{ eapply (lognat_monotonic H3). intuition. } generalize H3. rewrite <-Nat.mul_assoc. intros. rewrite <- (lognat_prod_sum H2). lia. Qed.
imports: ZArith micromega.Lia