proposition: Lemma rel_ls_lower_bound {found start} : rel_ls start found -> forall {k}, P k -> start <= k -> found <= k.
proof: Proof. induction 1 as [x p | x y no _ IH]; intros k pk greater. - exact greater. - destruct greater as [ | k greater]. + case (no pk). + apply (IH _ pk), le_n_S, greater. Qed.
imports: Arith