proposition: Lemma minus_neq_O : forall n i:nat, (i < n)%nat -> (n - i)%nat <> 0%nat.
proof: Proof. intros n i Hlt. apply Nat.neq_0_lt_0, Nat.lt_add_lt_sub_r; assumption. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun ArithRing