proposition: Lemma evenPathAux : forall l l' l'' lApp f n p, length l = (2 * n)%nat -> pathToPosAux (l ++ l' ++ l'') f = Some p -> exists f', pathToPosAux (l ++ l') f = pathToPosAux l' f' /\ pathToPosAux (l ++ l' ++ lApp) f = pathToPosAux (l' ++ lApp) f'.
proof: Proof. induction l using list_ind'. + intros. exists f. auto. + intros. simpl in *. lia. + intros l' l'' lApp f n p Len Valid. destruct n. - simpl in Len. congruence. - simpl in Len; assert (length l = (2 * n)%nat) by lia. destruct a eqn:A; destruct b eqn:B; simpl in *. * unfold pathToPos in Valid. simpl in Valid. pose proof (IHl l' l'' lApp (fun p => xO (f p)) n p H Valid) as Hyp; clear IHl H. inversion Hyp as [f' HF]; clear Hyp. exists f'. auto. * unfold pathToPos in Valid. simpl in Valid. pose proof (IHl l' l'' lApp (fun p => xI (f p)) n p H Valid) as Hyp; clear IHl H. inversion Hyp as [f' HF]; clear Hyp. exists f'. auto. * inversion Valid. * inversion Valid. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets