proposition: Theorem ltlePlusCompR : 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_lt_trans with (m := b + c); auto with stalmarck. apply Nat.add_lt_mono_l; auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)