proposition: Lemma lift_respects : forall q r, equiv q r -> equiv (lift q) (lift r).
proof: Proof. unfold equiv;simpl;intros q r E. rewrite <-2!preserves_mult. apply ap,E. Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields