proposition: Theorem NcountLe : forall (L1 L2 : list rNat) (S1 S2 : State), inclState S2 S1 -> Ncount S1 L2 L1 <= Ncount S2 L2 L1.
proof: Proof. intros L1; elim L1; simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)