proposition: Lemma tree_value_commmute_bis E c1 c2: echelon c1 -> echelon c2 -> \0c <c slength c1 -> \0c <c slength c2 -> echelon_to_tree c1 = echelon_to_tree c2 -> echelon_of_base c1 E = echelon_of_base c2 E.
proof: Proof. move => ha hb z1 z2. have i1: inc (cpred (slength c1)) (domain c1). move: (proj2 (proj1 (proj1 ha))) => lN. apply/(NltP lN); exact:(cpred_lt lN (nesym (proj2 z1))). have i2: inc (cpred (slength c2)) (domain c2). move: (proj2 (proj1 (proj1 hb))) => lN. apply/(NltP lN); exact:(cpred_lt lN (nesym (proj2 z2))). move: (tree_value_commutes E ha). move: (tree_value_commutes E hb). rewrite /echelon_of_base /echelon_to_tree /Vl. by move => -> ->; rewrite !LgV//; move => -> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)