proposition: Lemma le_minusni_n : forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat.
proof: Proof. intros n i _. induction i as [ | i IHi ]. - rewrite Nat.sub_0_r; reflexivity. - etransitivity; [ | apply IHi ]. rewrite Nat.sub_succ_r. apply Nat.le_pred_l. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun ArithRing