∀ m n, ex (λa. ex (λb. (((a × n) - (b × m)) = (gcd n m)) ∨ (((b × m) - (a × n)) = (gcd n m))))

Theorem eq_minus_gcd : forall (m:nat.nat), forall (n:nat.nat), connectives.ex (nat.nat) (fun (a:nat.nat) => connectives.ex (nat.nat) (fun (b:nat.nat) => connectives.Or (logic.eq (nat.nat) (nat.minus (nat.times a n) (nat.times b m)) (gcd n m)) (logic.eq (nat.nat) (nat.minus (nat.times b m) (nat.times a n)) (gcd n m)))).

theorem eq_minus_gcd : \forall (m:nat). \forall (n:nat). (ex) (nat) (\lambda a : nat. (ex) (nat) (\lambda b : nat. (Or) ((eq) (nat) ((minus) ((times) a n) ((times) b m)) ((gcd) n m)) ((eq) (nat) ((minus) ((times) b m) ((times) a n)) ((gcd) n m)))).

theorem eq_minus_gcd : forall (m:nat.nat) , forall (n:nat.nat) , ((connectives.ex) (nat.nat)) (fun (a : nat.nat) , ((connectives.ex) (nat.nat)) (fun (b : nat.nat) , (((connectives.Or) ) ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (a)) (n))) ((((nat.times) ) (b)) (m)))) ((((gcd.gcd) ) (n)) (m)))) ((((logic.eq_) (nat.nat)) ((((nat.minus) ) ((((nat.times) ) (b)) (m))) ((((nat.times) ) (a)) (n)))) ((((gcd.gcd) ) (n)) (m))))).

eq_minus_gcd : LEMMA (FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_ex[nat_sttfa_th.sttfa_nat]((LAMBDA(a:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_ex[nat_sttfa_th.sttfa_nat]((LAMBDA(b:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_Or(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(a)(n))(nat_sttfa_th.times(b)(m)))(gcd_sttfa.gcd(n)(m)))(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.times(b)(m))(nat_sttfa_th.times(a)(n)))(gcd_sttfa.gcd(n)(m)))))))))

Printing for OpenTheory is not working at the moment.