Suggest adding a tactic concerning parallel

[Autrilance]

When dealing with directions trivial things get messed up. For example, the process from Ray1.toDir = - Ray2.toDir to Seg1.toProj = Seg2.toProj has at least 2 steps of transformations. It may be of benifit to have a tactic concerning this issue.

[jjdishere]

At least we should have a tactic that gives one line universal proof of some trivial proofs of parallel, such as
LIN A B h \para SEG_nd B A h.symm by a_tactic
(Maybe weaker than you thought)