proposition: Lemma test_orb (a b c d : bool) : (a || b) || (c || d) = (a || c) || (b || d).
proof: Proof. time by rewrite orbACA. Restart. Proof. time by rewrite (AC (2*2) ((1*3)*(2*4))). Restart. Proof. time by rewrite orb.[AC (2*2) ((1*3)*(2*4))]. Qed.
imports: mathcomp(all_ssreflect ssralg)