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