proposition: Theorem ltStateLt : forall a b : rZ, In (valRz a) L -> In (valRz b) L -> forall S1 S2 : State, inclState S1 S2 -> eqStateRz S2 a b -> ~ eqStateRz S1 a b -> ltState S2 S1.
proof: Proof. intros a b H' H'0 S1 S2 H'1 H'2 H'3; red in |- *. apply vallStateLt with (a := a) (b := b); auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)