proposition: Lemma lengthNilOK {A : Type} : forall (l : list A), length l = 0 -> l = nil.
proof: Proof. intros l Hlength; induction l. reflexivity. simpl in Hlength. discriminate. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality