La prueba de Coq #Coq

Intento resolver esta prueba pero no encuentro cómo hacerlo.
Tengo dos objetivos pero ni siquiera sé si es correcto.

Aquí está el lema que intenté resolver con esto pero estoy atascado:

2 objetivos

a, b: Nat

H: Equal (leB a b) True

_______(1/2)

Equal match b with

| Z => False

| S m’ => leB a m’

end (leB a b) / Equal (leB b (S a)) (leB a b)

_______(2/2)

Equal (leB (S a) b) True / Equal (leB b (S a)) True

Inductive Bool : Type :=
          True : Bool | False : Bool.

Definition Not(b : Bool) : Bool :=
          Bool_rect (fun a => Bool)
                     False
                     True
                     b.

Lemma classic : forall b : Bool, Equal b (Not (Not b)).
Proof
intro.
induction b.
simpl.
apply refl.
simpl.
apply refl.
Qed.

Definition Equal(T : Type)(x y : T) : Prop :=
           forall P : T -> Prop, (P x) -> (P y).

Arguments Equal[T].
(* Avec certaines versions Arguments Equal[T] *)

Lemma refl : forall T : Type, forall x : T, Equal x x.
Proof
intros.
unfold Equal.
intros.
assumption.
Qed.

Fixpoint leB n m : Bool :=
  match n, m with
    | Z, _ => True
    | _, Z => False
    | S n', S m' => leB n' m'
  end.