proposition: Lemma tpairt_inv p : tpair (pairt p) = p.
proof: Proof. case: p => a b. rewrite /tpair /pairt /= /tmod. have ->: ∇(Δ(a + b) + b) = a + b. apply/eqP. rewrite trootE leq_addr /= deltaS. by rewrite addnS ltnS addnCA leq_addl. by rewrite [delta _ + _]addnC !addnK. Qed.
imports: mathcomp(all_ssreflect)