fact: Record mixin_of (T : Type) := Mixin { valid_op : T -> bool; join_op : T -> T -> T; unit_op : T; _ : commutative join_op; _ : associative join_op; _ : left_id unit_op join_op; _ : forall x y, valid_op (join_op x y) -> valid_op x; _ : valid_op unit_op }.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun)