proposition: Lemma sub_cancel_m : forall n i:nat, (i <= n -> n - (n - i) = i)%nat.
proof: Proof. intros. pose proof (Nat.sub_add i n H). apply Nat.add_sub_eq_l in H0. assumption. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits