> (fr′ n d d≢0) *fr (foo′ n' d' d'≢0) = fr′ (n * n') (d * d') dd'≢0 There doesn't seem to be a foo' constructor declared anywhere; is it a typo for fr'?