proposition: Lemma PosToPathPrefixFree : forall (x y : positive), (x <> y) -> PrefixFree [posToPath x; posToPath y].
proof: Proof. intros. destruct (Compare_dec.le_ge_dec (length (posToPathAux y)) (length (posToPathAux x))). + apply (PosToPathPrefixFreeAux H l). + apply prefixFreeCommutative. apply (@PosToPathPrefixFreeAux y x). - unfold not in *; intros; exfalso; auto. - auto. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets