proposition: Lemma ringinvmultgtandfun {X Y : ring} (f : ringfun X Y) (R : hrel Y) (isr : isinvringmultgt Y R) : isinvringmultgt X (λ x x', R (f x) (f x')).
proof: Proof. intros. set (ax0 := (pr2 (pr1 (pr2 f))) : (f 0) = 0). set (ax1 := (pr1 (pr2 (pr2 f))) : ∏ a b, paths (f (a * b)) ((f a) * (f b))). split. - intros a b rab ra. rewrite ax0 in ra. rewrite ax0 in rab. rewrite ax0. rewrite (ax1 _ _) in rab. apply ((pr1 isr) _ _ rab ra). - intros a b rab rb. rewrite ax0 in rb. rewrite ax0 in rab. rewrite ax0. rewrite (ax1 _ _) in rab. apply ((pr2 isr) _ _ rab rb). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids