fact: Definition mult_fin_r (alpha : t) (p : nat): t := match alpha, p with | (0,0), _ => zero | _, 0 => zero | (0, n), p => (0, n * p) | (n, b), n' => ( n * n', b) end.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)