proposition: Lemma le_plus_trans (n m p : nat) : (n <= m)%nat -> (n <= m + p)%nat.
proof: Proof. intro H; apply Nat.le_trans with m; [assumption | apply Nat.le_add_r]. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow