n m : pos_succ n = pos_succ m -> n = m. Proof. revert m. induction n as [ | n x | n x]; induction m as [ | m y | m y]. + reflexivity. + intro p. destruct (x0_neq_x1 p). + intro p. simpl in p. apply x0_inj in p. destruct m. 1,3: destruct (xH_neq_x0 p). destruct (xH_neq_x1 p). + intro p. destruct (x1_neq_x0 p). + simpl. intro p. by apply ap, x1_inj. + intro p. destruct (x1_neq_x0 p). + intro p. cbn in p. apply x0_inj in p. destruct n. 1,3: destruct (x0_neq_xH p). destruct (x1_neq_xH p). + intro p. cbn in p. destruct (x0_neq_x1 p). + intro p. apply ap, x, x0_inj, p. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Pos.Core.