proposition: Theorem NrelLt : forall (L1 : list rNat) (a : rNat) (b : rZ) (S1 S2 : State), inclState S1 S2 -> eqStateRz S2 (rZPlus a) b -> ~ eqStateRz S1 (rZPlus a) b -> In (valRz b) L1 -> Nrel S2 a L1 < Nrel S1 a L1.
proof: Proof. intros L1; elim L1; simpl in |- *; auto with stalmarck. intros a b S1 S2 H' H'0 H'1 H'2; elim H'2; auto with stalmarck. intros a l H' a0 b S1 S2 H'0 H'1 H'2 H'3; Elimc H'3; intros H'3; auto with stalmarck. rewrite H'3; auto with stalmarck. apply ltlePlusCompL; auto with stalmarck. change (oneStateAll S2 (valRz (rZPlus a0)) (valRz b) < oneStateAll S1 (valRz (rZPlus a0)) (valRz b)) in |- *; auto with stalmarck. apply ltlePlusCompR; auto with stalmarck. apply H' with (b := b); auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)