fact: Definition FF_div (e f:expr) : expr := let d := expr_div e f in match e, f with | expr_div e1 e2, expr_div f1 f2 => expr_div (PP_mult e1 f2) (PP_mult e2 f1) | _, _ => d end.
imports: CoRN.logic.CLogic Coq.Bool.Bool