text_formalization/tame/ssreflect/MQMSMAB-compiled.hl

   1 needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";;
   2 needs "../formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl";;
   3 needs "tame/CDTETAT.hl";;
   4 needs "tame/ssreflect/KCBLRQC-compiled.hl";;
   5
   6 (* Module Mqmsmab*)
   7 module Mqmsmab = struct
   8
   9 open Ssrbool;;
  10 open Ssrnat;;
  11 open Hypermap;;
  12 open Tame_lemmas;;
  13 open Tame_defs;;
  14 open Tame_general;;
  15 open Hypermap_and_fan;;
  16 open Hypermap_iso;;
  17 open Kcblrqc;;
  18 open Jgtdebu;;
  19 open Cdtetat_tame;;
  20 open Lp_ineqs_proofs;;
  21 open Lp_main_estimate;;
  22
  23 (* Section MQMSMAB *)
  24 Sections.begin_section "MQMSMAB";;
  25 (Sections.add_section_hyp "ineqs" (`kcblrqc_ineq_def`));;
  26 (Sections.add_section_hyp "h_main" (`lp_main_estimate`));;
  27
  28 (* Lemma MQMSMAB *)
  29 let MQMSMAB = Sections.section_proof ["V"]
  30 `contravening V ==> tame_hypermap (hypermap_of_fan (V, ESTD V))`
  31 [
  32    ((((use_arg_then2 ("tame_hypermap", [tame_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (move ["contrV"]));
  33    ((fun arg_tac -> (use_arg_then2 ("contravening_lp_fan", [contravening_lp_fan])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["h_fan"])));
  34    ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["fanV"])) THEN (case THEN (move ["f_surr"])) THEN (case THEN (move ["subV"])) THEN (move ["packV"])));
  35    ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH"]) THEN (move ["_"])))));
  36    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Crttxat_tame.CRTTXAT", [Crttxat_tame.CRTTXAT])) (fun fst_arg -> (use_arg_then2 ("JGTDEBU4", [JGTDEBU4])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_perimeter_bound", [fully_surrounded_perimeter_bound])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["card"])));
  37    ((((use_arg_then2 ("card", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card", [])) (disch_tac [])) THEN (clear_assumption "card") THEN BETA_TAC) THEN ((((use_arg_then2 ("tame_9a", [tame_9a]))(thm_tac (new_rewrite [] [])))) THEN (move ["card_ineq"])));
  38    ((((use_arg_then2 ("JGTDEBU10", [JGTDEBU10]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("JGTDEBU11", [JGTDEBU11]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SZIPOAS", [SZIPOAS]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("BDJYFFB1", [BDJYFFB1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
  39    ((((use_arg_then2 ("tame_1", [tame_1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU1", [JGTDEBU1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("JGTDEBU2", [JGTDEBU2]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
  40    ((((use_arg_then2 ("tame_2", [tame_2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU3", [JGTDEBU3]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("JGTDEBU4", [JGTDEBU4]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
  41    ((((use_arg_then2 ("tame_3", [tame_3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU5", [JGTDEBU5]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
  42    ((((use_arg_then2 ("tame_4", [tame_4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU6", [JGTDEBU6]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
  43    ((((use_arg_then2 ("tame_5a", [tame_5a]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU7", [JGTDEBU7]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
  44    ((((use_arg_then2 ("tame_8", [tame_8]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU8", [JGTDEBU8]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 12 0 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
  45    ((((use_arg_then2 ("tame_13a", [tame_13a]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("admissible_weight", [admissible_weight]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("total_weight", [total_weight]))(thm_tac (new_rewrite [] [])))));
  46    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
  47    ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`\f. tauVEF (V,ESTD V,f)`))) (term_tac exists_tac)) THEN (split_tac)));
  48    ((((use_arg_then2 ("REAL_LET_TRANS", [REAL_LET_TRANS])) (disch_tac [])) THEN (clear_assumption "REAL_LET_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`&4 * pi - &20 * sol0`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("tgt", [tgt]))(thm_tac (new_rewrite [] [])))));
  49    ((THENL_LAST) (split_tac) ((((use_arg_then2 ("Flyspeck_constants.bounds", [Flyspeck_constants.bounds])) (disch_tac [])) THEN (clear_assumption "Flyspeck_constants.bounds") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
  50    ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sum_tauVEF_upper_bound", [sum_tauVEF_upper_bound])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
  51    ((((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contrV", [])) (disch_tac [])) THEN (clear_assumption "contrV") THEN BETA_TAC) THEN (((((use_arg_then2 ("contravening", [contravening]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_gt", [real_gt]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  52    (((((use_arg_then2 ("adm_1", [adm_1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("adm_2", [adm_2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("adm_3", [adm_3]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac));
  53    (BETA_TAC THEN (move ["d"]) THEN (move ["d_in"]));
  54    ((fun arg_tac -> arg_tac (Arg_term (`CARD (face H d) = k ==> d IN darts_k k H`))) (term_tac (have_gen_tac ["k"](move ["d_in_k"]))));
  55    (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  56    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a >= 3 /\ a <= 6 ==> a = 3 \/ a = 4 \/ a = 5 \/ a = 6`))) (term_tac (have_gen_tac ["a"](move ["ineq"])))) ((arith_tac) THEN (done_tac)));
  57    (((fun arg_tac -> (use_arg_then2 ("card_ineq", [])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("ineq", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC);
  58    ((repeat_tactic 1 9 (case)) THEN (BETA_TAC THEN (move ["card_eq"])) THEN ((((use_arg_then2 ("card_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_tame", [d_tame]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_ge", [real_ge]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 20 (((use_arg_then2 ("ARITH_EQ", [ARITH_EQ]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))));
  59    ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau3_tauVEF_std", [ineq_tau3_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REFL_CLAUSE", [REFL_CLAUSE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in_k", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
  60    ((BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (move ["c"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  61    ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau4_tauVEF_std", [ineq_tau4_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REFL_CLAUSE", [REFL_CLAUSE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in_k", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
  62    ((BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (move ["c"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  63    ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau5_tauVEF_std", [ineq_tau5_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REFL_CLAUSE", [REFL_CLAUSE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in_k", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
  64    ((BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (move ["c"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  65    ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau6_tauVEF_std", [ineq_tau6_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REFL_CLAUSE", [REFL_CLAUSE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in_k", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
  66    ((BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (move ["c"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  67    ((split_tac) THEN (move ["d"]));
  68    (((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "r"))) THEN ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "p"))) THEN ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "q"))) THEN (BETA_TAC THEN (case THEN (move ["d_in"])) THEN (move ["r0"])));
  69    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`type_of_node H d = p,q,0`))) (term_tac (have_gen_tac [](move ["type_eq"])))) ((((use_arg_then2 ("type_of_node", [type_of_node]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
  70    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE KCBLRQC))) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("h_main", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineqs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
  71    (((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("type_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("LET_DEF", [LET_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LET_END_DEF", [LET_END_DEF]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("GT", [GT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LT_REFL", [LT_REFL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  72    ((BETA_TAC THEN (case THEN (move ["d_in"])) THEN (move ["type_eq"])) THEN ((((use_arg_then2 ("a_tame", [a_tame]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_ge", [real_ge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] []))))));
  73    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE BDJYFFB2))) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("h_main", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineqs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
  74    ((THENL_FIRST) (((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("type_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (ANTS_TAC)) ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
  75    ((fun arg_tac -> arg_tac (Arg_term (`GSPEC _`))) (term_tac (set_tac "s")));
  76    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`s = set_of_triangles_meeting_node H d`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac)));
  77    ((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("set_of_triangles_meeting_node", [set_of_triangles_meeting_node]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("set_of_face_meeting_node", [set_of_face_meeting_node]))(thm_tac (new_rewrite [] [])))));
  78    (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["f"]));
  79    ((THENL) (split_tac) [((case THEN ALL_TAC) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (move ["f_eq"]) THEN (move ["card_f"])); ((case THEN (move ["y"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y_in"])) THEN (case THEN (move ["card_f"])) THEN (move ["y_in_n"]) THEN (move ["f_eq"]))]);
  80    (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
  81    (((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [2] [])))) THEN (((use_arg_then2 ("card_f", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (done_tac));
  82 ];;
  83
  84 (* Finalization of the section MQMSMAB *)
  85 let MQMSMAB = Sections.finalize_theorem MQMSMAB;;
  86 Sections.end_section "MQMSMAB";;
  87
  88 (* Close the module *)
  89 end;;