proposition: Theorem cond_Zopp_Zlt_bool : forall m, cond_Zopp (Zlt_bool m 0) m = Z.abs m.
proof: Proof. intros m. apply sym_eq. case Zlt_bool_spec ; intros Hm. apply Zabs_non_eq. now apply Zlt_le_weak. now apply Z.abs_eq. Qed.
imports: Coq(ZArith Lia Zquot)