proposition: Lemma widen_3: forall N1 N2, ble N2 N1 = false -> (measure (widen N1 N2) < measure N1)%nat.
proof: Proof. unfold ble, measure; intros. destruct (isempty N2) eqn:E2. discriminate. destruct (isempty N1) eqn:E1. - unfold widen; rewrite E1, E2. generalize (Zinf.measure_1 (low N2)) (Zinf.measure_1 (high N2)). 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)); intros. destruct (Zinf.ble (high N2) (high N1)) eqn:LE. + cbn in H. apply Zinf.widen_3 in H. lia. + apply Zinf.widen_3 in LE. lia. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)