proposition: Lemma Exercise2_7A4: inductive NNstar.
proof: Proof. move: (Nat_order_wor) => [[or _] bs]. apply: Exercise2_7A2 => //. apply: (proj1 (opp_osr or)). exists \0c; apply: least_opposite =>//. have ns0 := NS0. split; first by rewrite bs. move => x; rewrite bs => xb; apply /Nat_order_leP; split => //. exact: (cle0n xb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)