fact: Fixpoint MM_plus (e f:expr) {struct e} : expr := let d := expr_plus e f in match e, f with | expr_mult (expr_var n) e', expr_mult (expr_var m) f' => match eq_nat n m with | true => MV_mult (MM_plus e' f') (expr_var n) | false => d end | expr_mult (expr_unop g arg) e', expr_mult (expr_unop h arg') f' => match eq_expr (expr_unop g arg) (expr_unop h arg') with | true => MV_mult (MM_plus e' f') (expr_unop g arg) | false => d end | expr_mult (expr_binop g e1 e2) e', expr_mult (expr_binop h f1 f2) f' => match eq_expr (expr_binop g e1 e2) (expr_binop h f1 f2) with | true => MV_mult (MM_plus e' f') (expr_binop g e1 e2) | false => d end | expr_mult (expr_part g arg) e', expr_mult (expr_part h arg') f' => match andb (eq_nat g h) (eq_expr arg arg') with | true => MV_mult (MM_plus e' f') (expr_part g arg) | false => d end | expr_int i, expr_int j => expr_int (i + j) | _, _ => d end.
imports: CoRN.logic.CLogic Coq.Bool.Bool