proposition: Theorem oneStateAllLt : forall (a b : rZ) (S1 S2 : State), inclState S1 S2 -> eqStateRz S2 a b -> ~ eqStateRz S1 a b -> oneStateAll S2 (valRz a) (valRz b) < oneStateAll S1 (valRz a) (valRz b).
proof: Proof. intros a b S1 S2 H'; unfold oneStateAll in |- *. case a; case b; simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)