proposition: Lemma nat_euclid_unique : forall i j q : nat, lt 0 q -> (i / q = j / q)%nat -> i mod q = j mod q -> i = j.
proof: Proof. intros. assert (q <> O). { destruct q. exfalso; exact (Nat.lt_irrefl O H). discriminate. } rewrite (Nat.div_mod j q H2), <- H1, <- H0. apply Nat.div_mod, H2. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile