proposition: Lemma factor_s_conv : forall(a : nat)(pf1 : (a <> 0))(pf2 : (S a) <> 0), (nat_to_pos (pf2)) = (Pos.succ (nat_to_pos pf1)).
proof: Proof. intros. destruct a. congruence. unfold nat_to_pos in *. simpl in *. intros. auto. Qed.
imports: ZArith micromega.Lia