nonzero_num@{} x : ~ (equiv x 0) <-> num x <> 0. Proof. split; intros E F; apply E. - red. rewrite F. simpl. rewrite 2!mult_0_l. reflexivity. - red in F;simpl in F. rewrite mult_1_r, mult_0_l in F. trivial. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.