proposition: Lemma list_size_tl_compat : forall (A : Set) (size : A -> nat) a b l, size a < size b -> list_size size (a :: l) < list_size size (b :: l).
proof: Proof. intros A size a b l H; simpl; apply plus_lt_compat_r; trivial. Qed.
imports: List Arith