proposition: Lemma in_seq len start n : In n (seq start len) <-> start <= n < start+len.
proof: Proof. revert start. induction len as [|len IHlen]; simpl; intros start. - rewrite Nat.add_0_r. split;[easy|]. intros (H,H'). apply (Nat.lt_irrefl start). eapply Nat.le_lt_trans; eassumption. - rewrite IHlen, Nat.add_succ_r; simpl; split. + intros [H|H]; subst; intuition. * apply -> Nat.succ_le_mono. apply Nat.le_add_r. * now apply Nat.lt_le_incl. + intros (H,H'). inversion H. * now left. * right. subst. now split; [apply -> Nat.succ_le_mono|]. Qed.
imports: PeanoNat