proposition: Lemma ble_2: forall N1 N2, le N1 N2 -> ble N1 N2 = true.
proof: Proof. unfold ble; intros. destruct N1. - apply le_Fin in H. destruct N2; auto. apply Z.leb_le; auto. - apply le_Inf in H. rewrite H. auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)