proposition: Lemma widen_2: forall N1 N2, (measure (widen N1 N2) <= (measure N1))%nat.
proof: Proof. unfold measure; intros. destruct (isempty N1) eqn:E1. unfold widen; rewrite E1. generalize (Zinf.measure_1 (low N2)) (Zinf.measure_1 (high N2)); intros. destruct (isempty N2); lia. destruct (isempty N2) eqn:E2. unfold widen; rewrite E1, E2, E1. lia. rewrite isempty_widen by auto. unfold widen; rewrite E1, E2; cbn. generalize (Zinf.widen_2 (low N1) (low N2)) (Zinf.widen_2 (high N1) (high N2)). lia. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)