proposition: Lemma le_plus_trans_rev: forall n m p : nat, n <= m -> n <= p + m.
proof: Proof. intros. assert (R: p + m = m + p). { apply Nat.add_comm. } rewrite R. apply Plus.le_plus_trans. assumption. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List