proposition: Lemma strong_binary_setoid_morphism_commutative {f : A → A → B} `{!Commutative f} `{∀ z, StrongSetoid_Morphism (f z)} : StrongSetoid_BinaryMorphism f.
proof: Proof. assert (∀ z, StrongSetoid_Morphism (λ x, f x z)). split; try apply _. intros x y. rewrite !(commutativity _ z). now apply (strong_extensionality (f z)). apply strong_binary_setoid_morphism_both_coordinates. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.jections