proposition: Lemma measure_map_lt: forall m1 m2, (forall x, V.measure (get x (Top_except m1)) <= V.measure (get x (Top_except m2)))%nat -> (exists x, V.measure (get x (Top_except m1)) < V.measure (get x (Top_except m2)))%nat -> (measure_map m1 < measure_map m2)%nat.
proof: Proof. intros m1 m2 LE (x & LT). rewrite (measure_map_remove m1 x), (measure_map_remove m2 x). assert ((measure_map (IdentMap.remove x m1) <= measure_map (IdentMap.remove x m2))%nat). { apply measure_map_le. intros y; unfold get. rewrite ! IMFact.remove_o. destruct (AbstrInterp.IdentMap.E.eq_dec x y). lia. apply LE. } lia. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)