proposition: Theorem PreWeakKonigsLemma : forall P, demorgan_inductively_barred_at P -> infinite_from P [] -> has_infinite_path P.
proof: Proof. intros P DeMorgan Hinf. exists (X P). intros l Hl. assert (infinite_from P l). { induction l. - assumption. - destruct Hl as (Hl,Ha). intros n. pose proof (IHl Hl) as IHl'. clear IHl. apply Y_approx in Hl; [|assumption]. destruct a. + destruct Ha as (l'&Hl'&HY'&n'&Hbar). rewrite (Y_unique _ DeMorgan _ _ Hl' HY' Hl) in Hbar. destruct (le_lt_dec n n') as [Hle|Hlt]. * specialize (IHl' (S n')). apply is_path_from_restrict with n'; [assumption|]. apply find_left_path; trivial. * specialize (IHl' (S n)). apply inductively_barred_at_monotone with (n:=n) in Hbar; [|apply Nat.lt_le_incl, Hlt]. apply find_left_path; trivial. + apply inductively_barred_at_imp_is_path_from; firstorder. } specialize (H 0). inversion H. assumption. Qed.
imports: WeakFan List Arith Compare_dec