proposition: Lemma Z2Qc_inj_sub n m : Qc_of_Z (n - m) = Qc_of_Z n - Qc_of_Z m.
proof: Proof. apply Qc_is_canon; simpl. by rewrite !Qred_correct, <-inject_Z_opp, <-inject_Z_plus. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)