proposition: Lemma 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: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.orders HoTT.Classes.implementations.peano_naturals HoTT.Classes.implementations.natpair_integers HoTT.Classes.theory.groups HoTT.Classes.theory.integers HoTT.Classes.theory.dec_fields HoTT.Classes.orders.dec_fields HoTT.Classes.orders.sum HoTT.Classes.theory.rationals HoTT.Classes.orders.lattices HoTT.Classes.implementations.assume_rationals HoTT.Classes.tactics.ring_quote HoTT.Classes.tactics.ring_tac