proposition: Lemma ble_2: forall N1 N2, le N1 N2 -> ble N1 N2 = true.
proof: Proof. unfold ble; intros. destruct (isempty N1) eqn:E; auto. destruct (nonempty_le N1 N2) as [P Q]; auto. apply andb_true_intro; split; apply Zinf.ble_2; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)