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