proposition: Lemma lengthPathEven : forall p, exists n, length (posToPathAux p) = (2 * n)%nat.
proof: Proof. induction p. + inversion IHp as [n Hyp]; clear IHp. simpl. exists (S n). rewrite app_length. rewrite Hyp. simpl. lia. + inversion IHp as [n Hyp]; clear IHp. simpl. exists (S n). rewrite app_length. rewrite Hyp. simpl. lia. + exists (O). simpl. auto. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets