proposition: Lemma seq_NoDup len start : NoDup (seq start len).
proof: Proof. revert start; induction len as [|len IH]; intros start; simpl; constructor; trivial. rewrite in_seq. intros (H,_). now apply (Nat.lt_irrefl start). Qed.
imports: PeanoNat