proposition: Lemma lognat_succ_h : forall a n (pf1 : n <> 0)(pf2: (S n) <> 0), a = lognat pf1 -> lognat pf2 = a \/ lognat pf2 = S (a).
proof: Proof. induction a; intros. assert (n = 1). apply (lognat_0_1 pf1). auto. subst. unfold lognat. simpl. auto. destruct (nat_comp n). destruct H0. subst. assert (x <> 0). lia. rewrite <- (lognat_prod_sum H0) in H. inversion H. subst. rewrite (lognat_odd _ pf1). rewrite <- (lognat_prod_sum H0). auto. subst. destruct (eq_nat_dec x 0). subst. unfold lognat in *. simpl in *. lia. generalize pf2. assert (S (S (2 * x)) = 2 * (S x)). lia. rewrite H0. intros. assert (S x <> 0). lia. assert (2 * x <> 0). lia. rewrite (lognat_odd _ H2) in H. rewrite <- (lognat_prod_sum n) in H. inversion H. rewrite <- (lognat_prod_sum H1). specialize (IHa x n H1 H4). destruct IHa. subst. rewrite H4. auto. subst. right. rewrite H3. auto. Qed.
imports: ZArith micromega.Lia