proposition: Lemma Separated_Refinement_lemma3 : forall H : 0 <= pred (m + n), Separated_Refinement_fun 0 H[=]a.
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; inversion b0. apply eq_symmetric_unfolded; apply partition_length_zero with Hab. cut (m + n <= 1); [ intro | lia ]. elim (plus_eq_one_imp_eq_zero _ _ H0); intro. rewrite <- a1; apply R. rewrite <- b1; apply P. exfalso; inversion b0. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)