proposition: Lemma le_Fin: forall n1 N2, le (Fin n1) N2 <-> In n1 N2.
proof: Proof. unfold le; cbn; intros; split; intros. - apply H. lia. - destruct N2; cbn in *; auto. lia. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)