proposition: Lemma triple_not_equal_zero : forall a b c : Z, ~ (a = 0%Z /\ b = 0%Z /\ c = 0%Z) -> a <> 0%Z \/ b <> 0%Z \/ c <> 0%Z.
proof: Proof. intros a b c H; case (Z_zerop a); intro Ha; [ case (Z_zerop b); intro Hb; [ case (Z_zerop c); intro Hc; [ apply False_ind; apply H; repeat split | right; right ] | right; left ] | left ]; assumption. Qed.
imports: Coq(Lia)