proposition: Lemma length_cons {T} (x : T) (xs : list T) : Datatypes.length (x :: xs) = S (Datatypes.length xs).
proof: Proof. reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround