proposition: Lemma rewrite_is_fun T (f : T -> T -> T) (a b c : T): commutative f -> associative f -> f (f b a) c = f a (f c b).
proof: Proof. move=> H1 H2. by rewrite [(f b a)]H1 -H2 [(f c b)]H1. Qed.
imports: mathcomp(ssreflect ssrfun eqtype ssrnat ssrbool)