proposition: Theorem ltStateTrans : transitive State ltState.
proof: Proof. red in |- *; unfold ltState in |- *; auto with stalmarck. intros S1 S2 S3 H' H'0. apply Nat.lt_trans with (m := valState S2); auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)