fact: Fixpoint term_eq (T : eqType)(t1 t2 : term T) := match t1, t2 with | Var n1, Var n2 => n1 == n2 | Const r1, Const r2 => r1 == r2 | NatConst n1, NatConst n2 => n1 == n2 | Add r1 s1, Add r2 s2 => (term_eq r1 r2) && (term_eq s1 s2) | Opp r1, Opp r2 => term_eq r1 r2 | NatMul r1 n1, NatMul r2 n2 => (term_eq r1 r2) && (n1 == n2) | Mul r1 s1, Mul r2 s2 => (term_eq r1 r2) && (term_eq s1 s2) | Inv r1, Inv r2 => term_eq r1 r2 | Exp r1 n1, Exp r2 n2 => (term_eq r1 r2) && (n1 == n2) |_, _ => false end.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)