let b, c be Nat; :: thesis: for a being positive Nat st b,c are_coprime & a + 1 divides b holds
not a + 1 divides c
let a be positive Nat; :: thesis: ( b,c are_coprime & a + 1 divides b implies not a + 1 divides c )
assume A1: ( b,c are_coprime & a + 1 divides b ) ; :: thesis: not a + 1 divides c
A2: a + 1 > 0 + 1 by XREAL_1:6;
assume a + 1 divides c ; :: thesis: contradiction
hence contradiction by A1, A2, PYTHTRIP:def 1; :: thesis: verum