for b, c being Nat
for a being positive Nat st b,c are_coprime & a + 1 divides b holds
not a + 1 divides c