Coinduction 1.7, tower-based, for Coq 8.16 and 8.17

• tower-based reimplementation of the tactic
  not backward compatible, but required changes should only result in simplifications
  (see changes in package coq-coinduction-examples)
  lemmas and definition related to the companion are kept in [companion.v]
• library should be loaded with [From Coinduction Require Import all].
• fixed efficiency issues with large arities
• compatible with both Coq 8.16 and 8.17