proposition: Lemma lt_absolu : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (x < y)%Z -> Z.abs_nat x < Z.abs_nat y.
proof: Proof. intros [| x| x] [| y| y] Hx Hy Hxy; inversion Hxy; try match goal with | id1:(0 <= Zneg _)%Z |- _ => apply False_ind; apply id1; constructor | id1:(Zpos _ <= 0)%Z |- _ => apply False_ind; apply id1; constructor | id1:(Zpos _ <= Zneg _)%Z |- _ => apply False_ind; apply id1; constructor end; simpl in |- *; apply lt_inj; repeat rewrite ZL9; assumption. Qed.
imports: Coq(Lia)