proposition: Lemma pathBeginsLeft : forall l1 l2 f x, l1 <> [] -> l2 <> [] -> pathToPosAux (l1 ++ l2) f = Some x -> head l1 = Some Left.
proof: Proof. destruct l1. + intros. exfalso; apply H; auto. + intros. destruct s. - auto. - simpl in H1. destruct (l1 ++ l2) eqn:Contra. * destruct l1; destruct l2; try solve [unfold not; exfalso; auto]; simpl in *; congruence. * congruence. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets