(R : Ring) (e f : R) `{IsOrthogonal R e f} : IsOrthogonal R f e := {| rng_idem_orth := rng_idem_orth' ; rng_idem_orth' := rng_idem_orth |}. Hint Immediate : typeclass_instances. Global Instance isorthogonal_op {R : Ring} (e f : R) `{r : IsOrthogonal R e f} : IsOrthogonal (rng_op R) e f. Proof. snrapply Build_IsOrthogonal. - exact (rng_idem_orth' (R:=R)). - exact (rng_idem_orth (R:=R)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids. Require Import Basics.Equivalences Basics.Trunc Types.Sigma WildCat.Core. Require Import Nat.Core Rings.Ring.