proposition: Lemma Zsgn_plus_l : forall a b : Z, Z.sgn a = Z.sgn b -> Z.sgn (a + b) = Z.sgn a.
proof: Proof. intros a b. case a; case b; simpl in |- *; auto; intros; try discriminate. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)