Coq et trivialites

[ghghgh]

Bonjour,

j'essaye de montrer en coq que pour tout entier (nat) n et m, on n < m -> n <> m.

Je n'y arrive malheureusement pas... j'ai essaye de faire une induction sur n ou m ou encore H : n < m, mais les sous-buts engendres (par exemple S n <> n et S a <> n... ou encore m <> 0 et m <> S n ne m'aident guere)

Sauriez-vous comment faire ?
merci d'avance !

[Doraki]

il faut faire une induction sur H : lt n m

ensuite tu fais auto ou simplify :/