proposition: Theorem lePlusComp : forall a b c d : nat, a <= b -> c <= d -> a + c <= b + d.
proof: Proof. intros a b c d H' H'0. apply Nat.le_trans with (m := a + d); auto with stalmarck. apply Nat.add_le_mono_l; auto with stalmarck. apply Nat.add_le_mono_r; auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)