proposition: Lemma anti_convert_pred_convert : forall p : positive, p = P_of_succ_nat (pred (nat_of_P p)).
proof: Proof. intro p. pattern p at 1 in |- *. rewrite <- pred_o_P_of_succ_nat_o_nat_of_P_eq_id. cut (exists n : nat, nat_of_P p = S n). intro H. elim H; intros x H0. rewrite H0. elim x. simpl in |- *. reflexivity. intros n H1. simpl in |- *. rewrite Pos.pred_succ. reflexivity. exists (pred (nat_of_P p)). symmetry; apply Nat.lt_succ_pred with 0. unfold nat_of_P in |- *. apply lt_O_positive_to_nat. auto with arith. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid