proposition: Lemma surj_cancel `{Countable A} `{EqDecision B} (f : A → B) `{!Surj (=) f} : { g : B → A & Cancel (=) f g }.
proof: Proof. exists (λ y, choose (λ x, f x = y) (surj f y)). intros y. by rewrite (choose_correct (λ x, f x = y) (surj f y)). Qed.
imports: Coq.QArith(QArith_base Qcanon) stdpp(well_founded) stdpp(options)