proposition: Lemma factor_double_conv : forall(a : nat)(pf1 : (a <> 0))(pf2 : (2 * a) <> 0), (nat_to_pos pf2) = (Pmult 2 (nat_to_pos pf1)).
proof: Proof. induction a; intros; simpl in *. congruence. destruct (eq_nat_dec a 0). subst. unfold nat_to_pos. auto. assert (a + S (a + 0) <> 0) by lia. specialize (factor_s_conv H). intros. unfold nat_to_pos in *. rewrite (H0 pf2). clear H0. clear pf2. assert (a + S (a + 0) = S (a + (a + 0))) by lia. rewrite H0. assert (a + (a + 0) <> 0) by lia. specialize (factor_s_conv H1). intros. unfold nat_to_pos in H2. rewrite <- H0 in H2. rewrite <- H0. rewrite (H2 H). clear H. clear H2. rewrite (IHa n). clear IHa. simpl. destruct a. intros. destruct n. auto. auto. lia. Qed.
imports: ZArith micromega.Lia