proposition: Lemma seq_nth : forall len start n d, n < len -> nth n (seq start len) d = start+n.
proof: Proof. intro len; induction len as [|len IHlen]; intros start n d H. - inversion H. - simpl seq. destruct n; simpl. + now rewrite Nat.add_0_r. + now rewrite IHlen; [rewrite Nat.add_succ_r|apply Nat.succ_lt_mono]. Qed.
imports: PeanoNat