proposition: Lemma can_inj {rT aT} {f: aT -> rT} {g: rT -> aT} (K: forall a, g (f a) = a) {a a'} (e: f a = f a') : a = a'.
proof: Proof. generalize (K a) (K a'). congruence. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63