proposition: Lemma Separated_Refinement_lemma1 : forall i j : nat, i = j -> forall (Hi : i <= pred (m + n)) (Hj : j <= pred (m + n)), Separated_Refinement_fun i Hi[=]Separated_Refinement_fun j Hj.
proof: Proof. do 3 intro. rewrite <- H; intros; unfold Separated_Refinement_fun in |- *; simpl in |- *. elim (le_lt_eq_dec _ _ Hi); elim (le_lt_eq_dec _ _ Hj); elim (le_lt_dec i 0); intros; simpl in |- *. algebra. apply RSR_h_nlnf; reflexivity. exfalso; rewrite <- b0 in a1; apply (Nat.lt_irrefl _ a1). exfalso; rewrite <- b1 in a0; apply (Nat.lt_irrefl _ a0). exfalso; rewrite <- b0 in a1; apply (Nat.lt_irrefl _ a1). exfalso; rewrite <- b1 in a0; apply (Nat.lt_irrefl _ a0). algebra. algebra. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)