∀ b c a, c ≤ b ⇒ (a - (b - c)) = ((a + c) - b)

Theorem minus_le_minus_minus_comm : forall (b:nat), forall (c:nat), forall (a:nat), (le c b) -> logic.eq (nat) (minus a (minus b c)) (minus (plus a c) b).

theorem minus_le_minus_minus_comm : \forall (b:nat). \forall (c:nat). \forall (a:nat). ((le) c b) -> (eq) (nat) ((minus) a ((minus) b c)) ((minus) ((plus) a c) b).

theorem minus_le_minus_minus_comm : forall (b:nat.nat) , forall (c:nat.nat) , forall (a:nat.nat) , ((((nat.le_) ) (c)) (b)) -> (((logic.eq_) (nat.nat)) ((((nat.minus) ) (a)) ((((nat.minus) ) (b)) (c)))) ((((nat.minus) ) ((((nat.plus) ) (a)) (c))) (b)).

minus_le_minus_minus_comm : LEMMA (FORALL(b:nat_sttfa.sttfa_nat):(FORALL(c:nat_sttfa.sttfa_nat):(FORALL(a:nat_sttfa.sttfa_nat):(nat_sttfa.le(c)(b) => logic_sttfa_th.eq[nat_sttfa.sttfa_nat](nat_sttfa.minus(a)(nat_sttfa.minus(b)(c)))(nat_sttfa.minus(nat_sttfa.plus(a)(c))(b))))))

Printing for OpenTheory is not working at the moment.