(x : F) Px : / x = // (x;Px). Proof. apply (left_cancellation_ne_0 (.*.) x). - apply trivial_apart. trivial. - rewrite dec_recip_inverse, reciperse_alt by (apply trivial_apart;trivial). reflexivity. Qed.
Require Import