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