proposition: Lemma recip_distr `{∀ z, PropHolds (z ≠ 0) → LeftCancellation (.*.) z} (x y : F ₀) : // (x * y) = // x * // y.
proof: Proof. destruct x, y. apply recip_distr_alt. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.fields