proposition: Lemma int_abs_nonneg x : 0 ≤ x -> f (int_abs Z N x) = x.
proof: Proof. intros E1. destruct (int_abs_spec x) as [[n E2]|[n E2]];trivial. assert (Hrw : x = 0). - apply (antisymmetry (<=));trivial. - rewrite Hrw,int_abs_0, (preserves_0 (f:=f)). trivial. Qed.
imports: HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.nat_int HoTT.Classes.theory.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.orders.rings