proposition: Theorem ltStateEqComp : forall S1 S2 S3 S4 : State, eqState S1 S3 -> eqState S2 S4 -> ltState S1 S2 -> ltState S3 S4.
proof: Proof. unfold eqState, ltState in |- *. intros S1 S2 S3 S4 H' H'0 H'1. Elimc H'0; intros H'0 H'2. Elimc H'; intros H' H'3. apply Nat.lt_le_trans with (m := valState S2); auto with stalmarck. apply Nat.le_lt_trans with (m := valState S1); auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)