coq-HoTT: How to prove 1 < 2?

I just would like to prove

Require Import HoTT. 
Open Scope nat. 

Lemma foo : 2 > 1. 

in coq-HoTT.
How to prove ?
Or, what is the tactic corresponding to auto which proves its counterpart in coq?