proposition: Lemma le_Inf: forall N, le Inf N <-> N = Inf.
proof: Proof. unfold le; intros; split; intros. - apply le_is_Inf with 0. intros; apply H; exact I. - subst N; exact I. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)