proposition: Theorem vallStateLtNEq : forall (L : list rNat) (S1 S2 : State), inclState S1 S2 -> eqState (restrictState S2 L) S2 -> ~ contradictory S2 -> ~ eqState S1 S2 -> valState L S2 < valState L S1.
proof: Proof. intros L S1 S2 H' H'0 Contr0 H'1. elim (inclStateDecBis S2 S1); intros H'2; auto with stalmarck. case H'1; red in |- *; auto with stalmarck. Elimc H'2; intros a E; Elimc E; intros b E; Elimc E; intros H'2 H'3. elim (InRestrictState S2 L a b); [ intros H'10 H'11 | idtac | idtac | idtac ]; auto with stalmarck. generalize H'2 H'3 H'10; clear H'2 H'3 H'10; Casec a; intros a H'2 H'3 H'4. apply vallStateLt with (a := rZPlus a) (b := b); auto with stalmarck. apply vallStateLt with (a := rZMinus a) (b := b); auto with stalmarck. apply eqStateRzSym; auto with stalmarck. apply eqStateEq with (S1 := S2); auto with stalmarck. Contradict H'3; rewrite H'3; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)