let pass = ALL_TAC;;
let qed = ASM_MESON_TAC;;
let intro = REPEAT STRIP_TAC;;
let havetac t tac = SUBGOAL_THEN t MP_TAC THENL [tac; pass] THEN DISCH_THEN(fun th -> ASSUME_TAC th);;
let have t why = havetac t(qed why);;
let choose n p why = have(mk_exists (n, p)) why THEN X_CHOOSE_TAC n(UNDISCH (TAUT (mk_imp (mk_exists (n, p), mk_exists (n, p)))));;

let le_minus_1_if_lt = prove(`
  !m n:num.
  m < n ==> m <= n-1
`,
  intro THEN
  choose `d:num` `n = m + SUC d` [LT_EXISTS] THEN
  have `n = m+(d+1)` [ADD1] THEN
  have `n = (m+d)+1` [ADD_ASSOC] THEN
  have `n = 1+(m+d)` [ADD_SYM] THEN
  have `n-1 = m+d` [ADD_SUB2] THEN
  qed[LE_EXISTS]
);;