proposition: Lemma double_not_equal_zero : forall c d : Z, ~ (c = 0%Z /\ d = 0%Z) -> c <> d \/ c <> 0%Z.
proof: Proof. intros. case (Z_zerop c). intro. rewrite e. left. apply sym_not_eq. intro. apply H; repeat split; assumption. intro; right; assumption. Qed.
imports: Coq(Lia)