proposition: Lemma RSR_auxR_lemma0 : RSR_auxR 0 = 0.
proof: Proof. unfold RSR_auxR in |- *. elim (le_lt_dec 0 0); intro; simpl in |- *. reflexivity. exfalso; inversion b0. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)