proposition: Lemma RSR_auxR_lemmam : RSR_auxR m = pred (m + n).
proof: Proof. unfold RSR_auxR in |- *. elim (le_lt_dec m 0); intro; simpl in |- *. cut (m = 0); [ intro | auto with arith ]. transitivity (pred m). rewrite H; auto. cut (0 = n); [ intro; rewrite <- H0; auto | apply RSR_HP' ]. apply partition_length_zero with Hab; rewrite <- H; apply R. elim (le_lt_dec m m); intro; simpl in |- *. rewrite Nat.sub_diag; auto. elim (Nat.lt_irrefl _ b1). Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)