Aは「n ≠ 0 (mod 3)」, Bは「n = 1 (mod 3)」,
Cは「n = 2 (mod 3)」, Dは「n² = 1 (mod 3)」です。

なぜ、Aの式には「≠」が付いているのでしょうか？
3で割って余りが0になるnという意味なら、「=」だと思いますが。
Aの言明は「整数nは3で割って余り0となるものではない」という意味なのでしょうか？
これを前提にすると、AはB「余り1」かC「余り2」のいずれかと同値になると考えられます。

Coqのコードでは、仮定Hypで「A <-> (B \/ C)」があり、最初のサブゴールに
「A -> D」という言明があります。これは自明ではないですが、
「B -> D」と「C -> D」の証明を使うことで、「A -> D」を示すことができるようです。
つまり、A, B, C, Dがモジュロ3で余り0の場合を除外した同値類であることを
示しているように思えます。どうでしょうか？