proposition: Lemma rangePosPrefixFree : forall p, PrefixFree (map posToPath (rangePos p)).
proof: Proof. intros. unfold rangePos. induction (Pos.to_nat p) as [ | n IHn]. + constructor. + simpl. apply FreeCons; auto. intros p' InP' p1 p2 App. apply in_map_iff in InP'. clear IHn. inversion InP' as [x xHyp]; clear InP'. inversion xHyp as [Pos2Path InX]; clear xHyp. subst. apply in_map_iff in InX. inversion InX as [y yHyp]; clear InX. inversion yHyp as [Pos2PathY InY]; clear yHyp. apply rangeNatLt in InY. inversion InY as [LtYSn YNotO]; clear InY. remember (match n with | O => 1 | S _ => Pos.succ (Pos.of_nat n) end) as m. assert (Neq : x <> m). unfold not; intros; subst. destruct y. - congruence. - destruct n. * lia. * assert (Pos.to_nat (Pos.of_nat (S y)) = Pos.to_nat (Pos.succ (Pos.of_nat (S n)))) by (rewrite H; auto). rewrite Pos2Nat.inj_succ in H0. rewrite Nat2Pos.id in H0. rewrite Nat2Pos.id in H0. + subst; lia. + congruence. + congruence. pose proof (@PosToPathPrefixFree x m) as Hyp. apply Hyp in Neq; clear Hyp. inversion Neq. eapply H2. + left; auto. + eauto. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets