ble_nat_true

Ble_nat_true.v

Theorem ble_nat_true : forall n m,
  ble_nat n m = true -> n <= m.
Proof.
  induction n as [|n'].
  Case "n' = 0".
    intros.
    induction m as [|m'].
    SCase "m' = 0".
      apply le_n.
    SCase "m' = S m".
      apply le_S.
      apply IHm'.
(* 2 subgoals, subgoal 1 (ID 4205) *)
  
(*   SCase := "m' = S m" : String.string *)
(*   Case := "n' = 0" : String.string *)
(*   m' : nat *)
(*   H : ble_nat 0 (S m') = true *)
(*   IHm' : ble_nat 0 m' = true -> 0 <= m' *)
(*   ============================ *)
(*    ble_nat 0 m' = true *)

(* subgoal 2 (ID 4182) is: *)
(*  forall m : nat, ble_nat (S n') m = true -> S n' <= m *)
      apply H.      (* Why is this satisfied?  Is it because forall (n : nat), 0 <= n? *)
  Case "n' = S n".
    intros.
    destruct m as [|m'].
    SCase "m' = 0".
      inversion H.
    SCase "m' = S m".
      inversion H.
      apply IHn' in H1.
      inversion H1.
      SSCase "n' = m'".
        reflexivity.
      SSCase "n' < m'".
        apply le_S.
        apply n_le_m__Sn_le_Sm.
        apply H0.
Qed.

apply does more than just applying. reflexivity could be used instead due to the way ble_nat is defined (by matching on the first argument).