fact: Fixpoint lt_expr (e f:expr) {struct e} : bool := match e, f with | expr_var n, expr_var m => lt_nat n m | expr_var n, _ => true | _, expr_var n => false | expr_int z, expr_int z' => lt_int z z' | expr_int _, _ => true | _, expr_int _ => false | expr_plus e1 e2, expr_plus f1 f2 => orb (lt_expr e1 f1) (andb (eq_expr e1 f1) (lt_expr e2 f2)) | expr_plus _ _, _ => true | _, expr_plus _ _ => false | expr_mult e1 e2, expr_mult f1 f2 => orb (lt_expr e1 f1) (andb (eq_expr e1 f1) (lt_expr e2 f2)) | expr_mult _ _, _ => true | _, expr_mult _ _ => false | expr_div e1 e2, expr_div f1 f2 => orb (lt_expr e1 f1) (andb (eq_expr e1 f1) (lt_expr e2 f2)) | expr_div _ _, _ => true | _, expr_div _ _ => false | expr_unop n e', expr_unop m f' => orb (lt_nat n m) (andb (eq_nat n m) (lt_expr e' f')) | expr_unop _ _, _ => true | _, expr_unop _ _ => false | expr_binop n e' e'', expr_binop m f' f'' => orb (lt_nat n m) (orb (andb (eq_nat n m) (lt_expr e' f')) (andb (eq_nat n m) (andb (eq_expr e' f') (lt_expr e'' f'')))) | expr_binop _ _ _, _ => true | _, expr_binop _ _ _ => false | expr_part n e', expr_part m f' => orb (lt_nat n m) (andb (eq_nat n m) (lt_expr e' f')) end.
imports: CoRN.logic.CLogic Coq.Bool.Bool