fact: Definition add (x y : Z3) : Z3 := match x, y with | z, _ => y | _, z => x | o, o => t | o, t | t, o => z | t, t => o end.
imports: mathcomp(all_ssreflect fingroup.fingroup fintype eqtype choice seq) deriving(deriving)