Q_triangular_one@{} : forall (q r : Q) (e : Q+) (Hqr : close e q r) (q0 : Q) (n : Q+), (close n q q0 -> close (e + n) r q0). Proof. unfold close;simpl. intros q r e [E1 E1'] s n [E2 E2']. split. - apply flip_lt_negate. rewrite negate_swap_r,!involutive. apply flip_lt_negate in E2. rewrite negate_swap_r,!involutive in E2. pose proof (plus_lt_compat _ _ _ _ E1' E2) as E. assert (Hrw : s - r = q - r + (s - q)) by abstract ring_tac.ring_with_integers (NatPair.Z nat). rewrite Hrw;trivial. - apply flip_lt_negate in E1. rewrite negate_swap_r,!involutive in E1. pose proof (plus_lt_compat _ _ _ _ E1 E2') as E. assert (Hrw : r - s = r - q + (q - s)) by abstract ring_tac.ring_with_integers (NatPair.Z nat). rewrite Hrw;trivial. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.