proposition: Lemma is_path_from_restrict : forall P n n' l, n <= n' -> is_path_from P n' l -> is_path_from P n l.
proof: Proof. intros * Hle H; induction H in n, Hle, H |- * ; intros. - apply Nat.le_0_r in Hle as ->. apply here. assumption. - destruct n. + apply here. assumption. + apply Nat.succ_le_mono in Hle. apply next_left; auto. - destruct n. + apply here. assumption. + apply Nat.succ_le_mono in Hle. apply next_right; auto. Qed.
imports: WeakFan List Arith Compare_dec