proposition: Lemma ble_2: forall N1 N2, le N1 N2 -> ble N1 N2 = true.
proof: Proof. unfold ble, le, In; intros. destruct N1; auto. - specialize (H n refl_equal). destruct N2. contradiction. apply Z.eqb_eq; auto. auto. - destruct N2. elim (H 0); auto. specialize (H (n + 1)); lia. auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)