theorem and_congruent_congruent: \forall m,n,a,b:nat. O < n \to O < m \to
gcd n m = (S O) \to ex nat (\lambda x. congruent x a m \land congruent x b n).
intros.
theorem and_congruent_congruent: \forall m,n,a,b:nat. O < n \to O < m \to
gcd n m = (S O) \to ex nat (\lambda x. congruent x a m \land congruent x b n).
intros.