FDL > PVS > Number Theory > gcd > gcd divides TCC1 > pf:gcd_divides_TCC1 : proof

Conclusion

1. FORALL i:int, j:int : ((i /= 0) OR (j /= 0)) IMPLIES ((i = 0) = > (j /= 0))