Establish isomorphism between finite natural numbers and sigma

I'm here with Coq studying the relations between two types I've defined. The first is something like a finite subset of nat, with just three elements:

Inductive N3 := zero | one | two.

The second is a sigma type with elements satisfying the proposition {x: nat | x < 3}. Here's its definition:

Definition less_than_3 := {x| x < 3}.

I want to prove that these two types are isomorphic. I definied the two functions involved in the following manner:

Definition lt3_to_N3 (n: less_than_3) : N3 :=
match n with
  | exist 0 _ => zero
  | exist 1 _ => one
  | exist 2 _ => two
  | exist _ _ => two
end.

Definition N3_to_lt3 (n: N3) : less_than_3 :=
match n with
  | zero => exist _ 0 l_0_3
  | one => exist _ 1 l_1_3
  | two => exist _ 2 l_2_3
end.

Where l_0_3, l_1_3, and l_2_3 are just axioms:

Axiom l_0_3 : 0 < 3.
Axiom l_1_3 : 1 < 3.
Axiom l_2_3 : 2 < 3.

I succeed in defining the first part of the isomorphism

Definition eq_n3_n3 (n: N3) : lt3_to_N3 (N3_to_lt3 n) = n.
Proof.
by case n.
Defined.

But I'm not able to define the other side. Here's what I've done so far:

Definition eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)).
Proof.
case: x.
move=> n p.
simpl.
???

I'm not sure at all about the rest of the definition. I also tried to pattern-match on x and on (N3_to_lt3 (lt3_to_N3 x)), but I'm not sure about what to return.

Definition eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)) :=
match N3_to_lt3 (lt3_to_N3 x) with
  | x => ???
end.

Thanks for the help.