proposition: Theorem oneStateLe : forall (a b : rZ) (S1 S2 : State), inclState S1 S2 -> oneState S2 a b <= oneState S1 a b.
proof: Proof. intros a b S1 S2 H'; unfold oneState in |- *. case (eqStateRzDec S1 a b); case (eqStateRzDec S2 a b); auto with stalmarck. intros H'0 H'1; case H'0; auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)