proposition: Lemma posPathInj : forall p, pathToPos (posToPath p) = Some p.
proof: Proof. induction p; unfold posToPath, pathToPos in *; simpl in *. - apply aux1 in IHp. inversion IHp as [f' Hyp]; clear IHp. rewrite <- app_assoc; simpl. pose proof Hyp [Left; Right; Right] as H; clear Hyp. inversion H as [H0 H1]; clear H. rewrite H0; clear H0. simpl; subst; auto. - apply aux1 in IHp. inversion IHp as [f' Hyp]; clear IHp. rewrite <- app_assoc; simpl. pose proof Hyp [Left; Left; Right] as H; clear Hyp. inversion H as [H0 H1]; clear H. rewrite H0; clear H0. simpl; subst; auto. - auto. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets