proposition: Lemma Separated_Refinement_lemma4 : forall H : pred (m + n) <= pred (m + n), Separated_Refinement_fun (pred (m + n)) H[=]b.
proof: Proof. intros; unfold Separated_Refinement_fun in |- *; simpl in |- *. elim (le_lt_eq_dec _ _ H); elim (le_lt_dec 0 0); intros; simpl in |- *. algebra. exfalso; apply (Nat.lt_irrefl _ a1). exfalso; apply (Nat.lt_irrefl _ a0). algebra. algebra. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)