Define relation [<=] on natural numbers by saying that [m <= n] holds if there is a number [k] such that [m = k + n]. 

Reflexive and transitive have been proved.

```
reflexive: ref: forall n:nat, n <= n.
transitive: trans: forall l m n:nat, l <= m -> m <= n -> l <= n

```

Now, how to prove `forall l m : nat, l <= m -> m <= l -> m = l`?