fact: Fixpoint MV_mult (e f:expr) {struct e} : expr := let d := expr_mult e f in match e, f with | expr_mult (expr_var n) e', expr_var m => match lt_nat n m with | true => expr_mult (expr_var n) (MV_mult e' f) | false => expr_mult f e end | expr_mult (expr_var n) e', expr_unop _ _ => expr_mult (expr_var n) (MV_mult e' f) | expr_mult (expr_var n) e', expr_binop _ _ _ => expr_mult (expr_var n) (MV_mult e' f) | expr_mult (expr_var n) e', expr_part _ _ => expr_mult (expr_var n) (MV_mult e' f) | expr_mult (expr_unop _ _) e', expr_var _ => expr_mult f e | expr_mult (expr_unop n e') e0, expr_unop m f' => match lt_expr (expr_unop n e') f with | true => expr_mult (expr_unop n e') (MV_mult e0 f) | false => expr_mult f e end | expr_mult (expr_unop n e1) e', expr_binop _ _ _ => expr_mult (expr_unop n e1) (MV_mult e' f) | expr_mult (expr_unop n e1) e', expr_part _ _ => expr_mult (expr_unop n e1) (MV_mult e' f) | expr_mult (expr_binop _ _ _) e', expr_var _ => expr_mult f e | expr_mult (expr_binop _ _ _) e', expr_unop _ _ => expr_mult f e | expr_mult (expr_binop n e' e'') e0, expr_binop m f' f'' => match lt_expr (expr_binop n e' e'') f with | true => expr_mult (expr_binop n e' e'') (MV_mult e0 f) | false => expr_mult f e end | expr_mult (expr_binop n e1 e2) e', expr_part _ _ => expr_mult (expr_binop n e1 e2) (MV_mult e' f) | expr_mult (expr_part _ _) e', expr_var _ => expr_mult f e | expr_mult (expr_part _ _) e', expr_unop _ _ => expr_mult f e | expr_mult (expr_part _ _) e', expr_binop _ _ _ => expr_mult f e | expr_mult (expr_part n e') e0, expr_part m f' => match lt_expr (expr_part n e') f with | true => expr_mult (expr_part n e') (MV_mult e0 f) | false => expr_mult f e end | expr_int i, f => MI_mult (expr_mult f expr_one) e | _, _ => d end.
imports: CoRN.logic.CLogic Coq.Bool.Bool